let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
let w be FinSequence of IAlph; :: thesis: for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
let tfsm, rtfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for q being State of tfsm
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
let q be State of tfsm; :: thesis: for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
let qr be State of rtfsm; :: thesis: ( rtfsm = the_reduction_of tfsm & q in qr implies for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k )
set TR = the Tran of tfsm;
assume that
A1: rtfsm = the_reduction_of tfsm and
A2: q in qr ; :: thesis: for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
defpred S₁[ Nat] means ( $1 in Seg ((len w) + 1) implies ((q,w) -admissible) . $1 in ((qr,w) -admissible) . $1 );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: ( k in Seg ((len w) + 1) implies ((q,w) -admissible) . k in ((qr,w) -admissible) . k ) ; :: thesis: S₁[k + 1]
assume A5: k + 1 in Seg ((len w) + 1) ; :: thesis: ((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)
A6: ( k = 0 or ( 0 < k & 0 + 1 = 1 ) ) ;

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

suppose A7: k = 0 ; :: thesis: ((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)

then ((q,w) -admissible) . (k + 1) = q by Def2;
hence ((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1) by A2, A7, Def2; :: thesis: verum

end;

suppose A8: 1 <= k ; :: thesis: ((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)

A9: k + 1 <= (len w) + 1 by A5, FINSEQ_1:1;
then A10: k <= len w by XREAL_1:6;
then consider w1i being Element of IAlph, q1i, q1i1 being Element of tfsm such that
A11: ( w1i = w . k & q1i = ((q,w) -admissible) . k ) and
A12: ( q1i1 = ((q,w) -admissible) . (k + 1) & w1i -succ_of q1i = q1i1 ) by A8, Def2;
consider w2i being Element of IAlph, q2i, q2i1 being Element of rtfsm such that
A13: ( w2i = w . k & q2i = ((qr,w) -admissible) . k ) and
A14: ( q2i1 = ((qr,w) -admissible) . (k + 1) & w2i -succ_of q2i = q2i1 ) by A8, A10, Def2;
k <= k + 1 by NAT_1:11;
then k <= (len w) + 1 by A9, XXREAL_0:2;
then the Tran of tfsm . (q1i,w1i) in the Tran of rtfsm . (q2i,w2i) by A1, A4, A8, A11, A13, Def18, FINSEQ_1:1;
hence ((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1) by A12, A14; :: thesis: verum

end;

end;

end;

A15: S₁[ 0 ] by FINSEQ_1:1;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A3); :: thesis: verum