let IAlph, OAlph be non empty set ; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic holds
tfsm1,tfsm2 -are_equivalent
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( tfsm1,tfsm2 -are_isomorphic implies tfsm1,tfsm2 -are_equivalent )
assume tfsm1,tfsm2 -are_isomorphic ; :: thesis: tfsm1,tfsm2 -are_equivalent
then consider Tf being Function of the carrier of tfsm1,the carrier of tfsm2 such that
Tf is bijective and
A1: Tf . the InitS of tfsm1 = the InitS of tfsm2 and
A2: for q being Element of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) by Def19;

now

let w1 be FinSequence of IAlph; :: thesis: the InitS of tfsm1,w1 -response = the InitS of tfsm2,w1 -response
set rw1 = the InitS of tfsm1,w1 -response ;
set rw2 = the InitS of tfsm2,w1 -response ;
set aw1 = the InitS of tfsm1,w1 -admissible ;
set aw2 = the InitS of tfsm2,w1 -admissible ;
A3: for k being Element of NAT st 1 <= k & k <= (len w1) + 1 holds
Tf . ((the InitS of tfsm1,w1 -admissible ) . k) = (the InitS of tfsm2,w1 -admissible ) . k

proof

defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= (len w1) + 1 implies Tf . ((the InitS of tfsm1,w1 -admissible ) . $1) = (the InitS of tfsm2,w1 -admissible ) . $1 );
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: ( 1 <= k & k <= (len w1) + 1 implies Tf . ((the InitS of tfsm1,w1 -admissible ) . k) = (the InitS of tfsm2,w1 -admissible ) . k ) ; :: thesis: S₁[k + 1]
assume that
1 <= k + 1 and
A6: k + 1 <= (len w1) + 1 ; :: thesis: Tf . ((the InitS of tfsm1,w1 -admissible ) . (k + 1)) = (the InitS of tfsm2,w1 -admissible ) . (k + 1)
A7: ( 0 = k or ( 0 < k & 0 + 1 = 1 ) ) ;

per cases ( 0 = k or 1 <= k ) by A7, NAT_1:13;

suppose A8: 0 = k ; :: thesis: Tf . ((the InitS of tfsm1,w1 -admissible ) . (k + 1)) = (the InitS of tfsm2,w1 -admissible ) . (k + 1)

hence Tf . ((the InitS of tfsm1,w1 -admissible ) . (k + 1)) = the InitS of tfsm2 by A1, Def2
.= (the InitS of tfsm2,w1 -admissible ) . (k + 1) by A8, Def2 ;
:: thesis: verum

end;

suppose A9: 1 <= k ; :: thesis: Tf . ((the InitS of tfsm1,w1 -admissible ) . (k + 1)) = (the InitS of tfsm2,w1 -admissible ) . (k + 1)

A10: len w1 <= (len w1) + 1 by NAT_1:11;
A11: k <= len w1 by A6, XREAL_1:8;
then consider w1k being Element of IAlph, qk, qk1 being Element of tfsm1 such that
A12: ( w1k = w1 . k & qk = (the InitS of tfsm1,w1 -admissible ) . k ) and
A13: ( qk1 = (the InitS of tfsm1,w1 -admissible ) . (k + 1) & w1k -succ_of qk = qk1 ) by A9, Def2;
consider w2k being Element of IAlph, q2k, q2k1 being Element of tfsm2 such that
A14: ( w2k = w1 . k & q2k = (the InitS of tfsm2,w1 -admissible ) . k ) and
A15: ( q2k1 = (the InitS of tfsm2,w1 -admissible ) . (k + 1) & w2k -succ_of q2k = q2k1 ) by A9, A11, Def2;
thus Tf . ((the InitS of tfsm1,w1 -admissible ) . (k + 1)) = Tf . (the Tran of tfsm1 . qk,w1k) by A13
.= the Tran of tfsm2 . q2k,w2k by A2, A5, A9, A11, A12, A14, A10, XXREAL_0:2
.= (the InitS of tfsm2,w1 -admissible ) . (k + 1) by A15 ; :: thesis: verum

end;

end;

end;

A16: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A16, A4); :: thesis: verum

end;

A17: now

let k be Nat; :: thesis: ( 1 <= k & k <= len (the InitS of tfsm1,w1 -response ) implies (the InitS of tfsm2,w1 -response ) . k = (the InitS of tfsm1,w1 -response ) . k )
assume that
A18: 1 <= k and
A19: k <= len (the InitS of tfsm1,w1 -response ) ; :: thesis: (the InitS of tfsm2,w1 -response ) . k = (the InitS of tfsm1,w1 -response ) . k
k <= len w1 by A19, Def6;
then A20: k in dom w1 by A18, FINSEQ_3:27;
then A21: w1 . k is Element of IAlph by FINSEQ_2:13;
k in Seg (len w1) by A20, FINSEQ_1:def 3;
then k in Seg ((len w1) + 1) by FINSEQ_2:9;
then k in Seg (len (the InitS of tfsm1,w1 -admissible )) by Def2;
then A22: k in dom (the InitS of tfsm1,w1 -admissible ) by FINSEQ_1:def 3;
then A23: 1 <= k by FINSEQ_3:27;
k <= len (the InitS of tfsm1,w1 -admissible ) by A22, FINSEQ_3:27;
then A24: k <= (len w1) + 1 by Def2;
A25: k in NAT by ORDINAL1:def 13;
A26: (the InitS of tfsm1,w1 -admissible ) . k is Element of tfsm1 by A22, FINSEQ_2:13;
thus (the InitS of tfsm2,w1 -response ) . k = the OFun of tfsm2 . [((the InitS of tfsm2,w1 -admissible ) . k),(w1 . k)] by A20, Def6
.= the OFun of tfsm2 . (Tf . ((the InitS of tfsm1,w1 -admissible ) . k)),(w1 . k) by A3, A23, A24, A25
.= the OFun of tfsm1 . ((the InitS of tfsm1,w1 -admissible ) . k),(w1 . k) by A2, A26, A21
.= (the InitS of tfsm1,w1 -response ) . k by A20, Def6 ; :: thesis: verum

end;

len (the InitS of tfsm1,w1 -response ) = len w1 by Def6
.= len (the InitS of tfsm2,w1 -response ) by Def6 ;
hence the InitS of tfsm1,w1 -response = the InitS of tfsm2,w1 -response by A17, FINSEQ_1:18; :: thesis: verum

end;

hence tfsm1,tfsm2 -are_equivalent by Def9; :: thesis: verum