let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for k being Nat st Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) holds
for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for k being Nat st Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) holds
for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
let k be Nat; :: thesis: ( Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) implies for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm) )
set S = the carrier of tfsm;
set CEk = Class (k -eq_states_EqR tfsm);
set Ek = k -eq_states_EqR tfsm;
set CEk1 = Class ((k + 1) -eq_states_EqR tfsm);
set Ek1 = (k + 1) -eq_states_EqR tfsm;
defpred S₁[ Nat] means Class ((k + $1) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm);
assume Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) ; :: thesis: for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
then A1: k -eq_states_EqR tfsm = (k + 1) -eq_states_EqR tfsm by FINSEQ_4:86;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
set CEkm = Class ((k + m) -eq_states_EqR tfsm);
set Ekm = (k + m) -eq_states_EqR tfsm;
set CEkm1 = Class ((k + (m + 1)) -eq_states_EqR tfsm);
set Ekm1 = (k + (m + 1)) -eq_states_EqR tfsm;
assume Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm) ; :: thesis: S₁[m + 1]
then A3: (k + m) -eq_states_EqR tfsm = k -eq_states_EqR tfsm by FINSEQ_4:86;

now :: thesis: for x being object holds
( ( x in Class ((k + (m + 1)) -eq_states_EqR tfsm) implies x in Class (k -eq_states_EqR tfsm) ) & ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) ) )

let x be object ; :: thesis: ( ( x in Class ((k + (m + 1)) -eq_states_EqR tfsm) implies x in Class (k -eq_states_EqR tfsm) ) & ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) ) )
reconsider xx = x as set by TARSKI:1;

hereby :: thesis: ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) )

assume A4: x in Class ((k + (m + 1)) -eq_states_EqR tfsm) ; :: thesis: x in Class (k -eq_states_EqR tfsm)
then reconsider x9 = x as Subset of the carrier of tfsm ;
consider qa being object such that
A5: qa in the carrier of tfsm and
A6: x9 = Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) by A4, EQREL_1:def 3;
reconsider qa = qa as Element of the carrier of tfsm by A5;
A7: x9 c= the carrier of tfsm ;

now :: thesis: for y being object holds
( ( y in xx implies y in Class ((k -eq_states_EqR tfsm),qa) ) & ( y in Class ((k -eq_states_EqR tfsm),qa) implies y in xx ) )

let y be object ; :: thesis: ( ( y in xx implies y in Class ((k -eq_states_EqR tfsm),qa) ) & ( y in Class ((k -eq_states_EqR tfsm),qa) implies y in xx ) )

hereby :: thesis: ( y in Class ((k -eq_states_EqR tfsm),qa) implies y in xx )

assume A8: y in xx ; :: thesis: y in Class ((k -eq_states_EqR tfsm),qa)
then reconsider y9 = y as Element of the carrier of tfsm by A7;
[y,qa] in (k + (m + 1)) -eq_states_EqR tfsm by A6, A8, EQREL_1:19;
then k + (m + 1) -equivalent y9,qa by Def12;
then k -equivalent y9,qa by Th26;
then [y9,qa] in k -eq_states_EqR tfsm by Def12;
hence y in Class ((k -eq_states_EqR tfsm),qa) by EQREL_1:19; :: thesis: verum

end;

assume A9: y in Class ((k -eq_states_EqR tfsm),qa) ; :: thesis: y in xx
then reconsider y9 = y as Element of the carrier of tfsm ;
[y9,qa] in k -eq_states_EqR tfsm by A9, EQREL_1:19;
then A10: k + 1 -equivalent y9,qa by A1, Def12;
A11: 1 <= k + 1 by NAT_1:11;

A12: now :: thesis: for s being Element of IAlph
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]

let s be Element of IAlph; :: thesis: for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]
let k1 be Nat; :: thesis: ( k1 = ((k + m) + 1) - 1 implies k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] )
set Sy9 = the Tran of tfsm . [y9,s];
set Sqa = the Tran of tfsm . [qa,s];
( k in NAT & k = (k + 1) - 1 ) by ORDINAL1:def 12;
then k -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] by A10, A11, Th27;
then A13: [( the Tran of tfsm . [y9,s]),( the Tran of tfsm . [qa,s])] in k -eq_states_EqR tfsm by Def12;
assume k1 = ((k + m) + 1) - 1 ; :: thesis: k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]
hence k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] by A3, A13, Def12; :: thesis: verum

end;

( 1 <= (k + m) + 1 & 1 -equivalent y9,qa ) by A10, A11, Th27, NAT_1:11;
then (k + m) + 1 -equivalent y9,qa by A12, Th27;
then [y9,qa] in (k + (m + 1)) -eq_states_EqR tfsm by Def12;
hence y in xx by A6, EQREL_1:19; :: thesis: verum

end;

then x = Class ((k -eq_states_EqR tfsm),qa) by TARSKI:2;
hence x in Class (k -eq_states_EqR tfsm) by EQREL_1:def 3; :: thesis: verum

end;

assume A14: x in Class (k -eq_states_EqR tfsm) ; :: thesis: x in Class ((k + (m + 1)) -eq_states_EqR tfsm)
then reconsider x9 = x as Subset of the carrier of tfsm ;
consider qa being object such that
A15: qa in the carrier of tfsm and
A16: x9 = Class ((k -eq_states_EqR tfsm),qa) by A14, EQREL_1:def 3;
reconsider qa = qa as Element of the carrier of tfsm by A15;

now :: thesis: for y being object holds
( ( y in xx implies y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) ) & ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx ) )

let y be object ; :: thesis: ( ( y in xx implies y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) ) & ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx ) )

hereby :: thesis: ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx )

assume A17: y in xx ; :: thesis: y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa)
then reconsider y9 = y as Element of the carrier of tfsm by A16;
[y9,qa] in k -eq_states_EqR tfsm by A16, A17, EQREL_1:19;
then A18: k + 1 -equivalent y9,qa by A1, Def12;
A19: 1 <= k + 1 by NAT_1:11;

A20: now :: thesis: for s being Element of IAlph
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]

let s be Element of IAlph; :: thesis: for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]
let k1 be Nat; :: thesis: ( k1 = ((k + m) + 1) - 1 implies k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] )
set Sy9 = the Tran of tfsm . [y9,s];
set Sqa = the Tran of tfsm . [qa,s];
( k in NAT & k = (k + 1) - 1 ) by ORDINAL1:def 12;
then k -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] by A18, A19, Th27;
then A21: [( the Tran of tfsm . [y9,s]),( the Tran of tfsm . [qa,s])] in k -eq_states_EqR tfsm by Def12;
assume k1 = ((k + m) + 1) - 1 ; :: thesis: k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]
hence k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] by A3, A21, Def12; :: thesis: verum

end;

( 1 <= (k + m) + 1 & 1 -equivalent y9,qa ) by A18, A19, Th27, NAT_1:11;
then (k + m) + 1 -equivalent y9,qa by A20, Th27;
then [y9,qa] in (k + (m + 1)) -eq_states_EqR tfsm by Def12;
hence y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) by EQREL_1:19; :: thesis: verum

end;

assume A22: y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) ; :: thesis: y in xx
then reconsider y9 = y as Element of the carrier of tfsm ;
[y,qa] in (k + (m + 1)) -eq_states_EqR tfsm by A22, EQREL_1:19;
then k + (m + 1) -equivalent y9,qa by Def12;
then k -equivalent y9,qa by Th26;
then [y9,qa] in k -eq_states_EqR tfsm by Def12;
hence y in xx by A16, EQREL_1:19; :: thesis: verum

end;

then x = Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) by TARSKI:2;
hence x in Class ((k + (m + 1)) -eq_states_EqR tfsm) by EQREL_1:def 3; :: thesis: verum

end;

hence Class ((k + (m + 1)) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm) by TARSKI:2; :: thesis: verum

end;

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