let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k
let fsm be non empty FSM over IAlph; :: thesis: for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k
let w1, w2 be FinSequence of IAlph; :: thesis: for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k
let q1, q2 be State of fsm; :: thesis: ( q1,w1 -leads_to q2 implies for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k )
set q1w = (q1,(w1 ^ w2)) -admissible ;
set q2w2 = (q2,w2) -admissible ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= (len w2) + 1 implies ((q1,(w1 ^ w2)) -admissible) . ((len w1) + $1) = ((q2,w2) -admissible) . $1 );
assume A1: q1,w1 -leads_to q2 ; :: thesis: for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -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 w2) + 1 implies ((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k ) ; :: thesis: S₁[k + 1]
assume that
1 <= k + 1 and
A4: k + 1 <= (len w2) + 1 ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . ((len w1) + (k + 1)) = ((q2,w2) -admissible) . (k + 1)

per cases ( k = 0 or 0 < k ) ;

suppose A5: k = 0 ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . ((len w1) + (k + 1)) = ((q2,w2) -admissible) . (k + 1)

hence ((q1,(w1 ^ w2)) -admissible) . ((len w1) + (k + 1)) = q2 by A1, Th6
.= ((q2,w2) -admissible) . (k + 1) by A5, Def2 ;
:: thesis: verum

end;

suppose A6: 0 < k ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . ((len w1) + (k + 1)) = ((q2,w2) -admissible) . (k + 1)

A7: k <= len w2 by A4, XREAL_1:6;
A8: 0 + 1 = 1 ;
then 1 <= k by A6, NAT_1:13;
then A9: ( ex w2i being Element of IAlph ex q2i, q2i1 being State of fsm st
( w2i = w2 . k & q2i = ((q2,w2) -admissible) . k & q2i1 = ((q2,w2) -admissible) . (k + 1) & w2i -succ_of q2i = q2i1 ) & k in dom w2 ) by A7, Def2, FINSEQ_3:25;
len (w1 ^ w2) = (len w1) + (len w2) by FINSEQ_1:22;
then A10: (len w1) + k <= len (w1 ^ w2) by A7, XREAL_1:7;
1 <= (len w1) + k by A6, A8, NAT_1:13;
then ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = (w1 ^ w2) . ((len w1) + k) & qi = ((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) & qi1 = ((q1,(w1 ^ w2)) -admissible) . (((len w1) + k) + 1) & wi -succ_of qi = qi1 ) by A10, Def2;
hence ((q1,(w1 ^ w2)) -admissible) . ((len w1) + (k + 1)) = ((q2,w2) -admissible) . (k + 1) by A3, A4, A6, A8, A9, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

end;

end;

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