A1:Automata(Alph;S1), A2:Automata(Alph;S2).
Con(A1) & Con(A2) 
LangOf(A1) = LangOf(A2) A1 
A2 & A2 A1 A1 
A2
refine_iso
A2
== 
f:(S1
S2).
Bij(S1; S2; f)
& (s:S1, a:Alph. f(
A1(s,a)) = A2(f(s),a))
& f(InitialState(A1)) = InitialState(A2)
& (s:S1. FinalState(A1)(s) = FinalState(A2)(f(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). A1 A2 A2 A1
auto_iso_sym