let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let w be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let q11 be State of tfsm1; :: thesis: for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let Tf be Function of the carrier of tfsm1, the carrier of tfsm2; :: thesis: ( ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) implies for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k )
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= (len w) + 1 implies Tf . (((q11,w) -admissible) . $1) = (((Tf . q11),w) -admissible) . $1 );
assume A1: for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ; :: thesis: for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: ( 1 <= k & k <= (len w) + 1 implies Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k ) ; :: thesis: S₁[k + 1]
assume that
1 <= k + 1 and
A4: k + 1 <= (len w) + 1 ; :: thesis: Tf . (((q11,w) -admissible) . (k + 1)) = (((Tf . q11),w) -admissible) . (k + 1)
A5: ( k = 0 or ( 0 < k & 0 + 1 = 1 ) ) ;

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

suppose A6: k = 0 ; :: thesis: Tf . (((q11,w) -admissible) . (k + 1)) = (((Tf . q11),w) -admissible) . (k + 1)

hence Tf . (((q11,w) -admissible) . (k + 1)) = Tf . q11 by Def2
.= (((Tf . q11),w) -admissible) . (k + 1) by A6, Def2 ;
:: thesis: verum

end;

suppose A7: 1 <= k ; :: thesis: Tf . (((q11,w) -admissible) . (k + 1)) = (((Tf . q11),w) -admissible) . (k + 1)

A8: len w <= (len w) + 1 by NAT_1:11;
A9: k <= len w by A4, XREAL_1:6;
then consider wi being Element of IAlph, qi, qi1 being State of tfsm1 such that
A10: ( wi = w . k & qi = ((q11,w) -admissible) . k ) and
A11: ( qi1 = ((q11,w) -admissible) . (k + 1) & wi -succ_of qi = qi1 ) by A7, Def2;
consider wri being Element of IAlph, qri, qri1 being State of tfsm2 such that
A12: ( wri = w . k & qri = (((Tf . q11),w) -admissible) . k ) and
A13: ( qri1 = (((Tf . q11),w) -admissible) . (k + 1) & wri -succ_of qri = qri1 ) by A7, A9, Def2;
thus Tf . (((q11,w) -admissible) . (k + 1)) = Tf . ( the Tran of tfsm1 . (qi,wi)) by A11
.= the Tran of tfsm2 . (qri,wri) by A1, A3, A7, A9, A8, A10, A12, XXREAL_0:2
.= (((Tf . q11),w) -admissible) . (k + 1) by A13 ; :: thesis: verum

end;

end;

end;

A14: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A2); :: thesis: verum