A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) 
LangOf(A1) = LangOf(A2) A1 
A2 & A2 A1 A1 
A2
refine_iso
s:St. 
l:Alph*. (Result(A)l) = s
Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) LangOf(A1) = LangOf(A2) A1 A2 & A2 A1 A1 A2
refine_iso
Thm* A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) A1 A2 |S1| 
|S2|
refine_ge