1 | f:(St (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))).
Bij(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); f)
& ( s:St, a:Alph.
f( Auto(s,a)) = A( l.Auto(l) )(f(s),a) x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
& f(InitialState(Auto)) = InitialState(A( l.Auto(l) )) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
& ( s:St. FinalState(Auto)(s) = FinalState(A( l.Auto(l) ))(f(s))) |