let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1 being State of fsm
for k being Nat st 1 <= k & k <= len w1 holds
((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k
let fsm be non empty FSM over IAlph; :: thesis: for w1, w2 being FinSequence of IAlph
for q1 being State of fsm
for k being Nat st 1 <= k & k <= len w1 holds
((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k
let w1, w2 be FinSequence of IAlph; :: thesis: for q1 being State of fsm
for k being Nat st 1 <= k & k <= len w1 holds
((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k
let q1 be State of fsm; :: thesis: for k being Nat st 1 <= k & k <= len w1 holds
((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k
set q1w = (q1,(w1 ^ w2)) -admissible ;
set q1w1 = (q1,w1) -admissible ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len w1 implies ((q1,(w1 ^ w2)) -admissible) . $1 = ((q1,w1) -admissible) . $1 );

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume that
1 <= k + 1 and
A3: k + 1 <= len w1 ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . (k + 1) = ((q1,w1) -admissible) . (k + 1)
A4: ( 0 = k or ( 0 < k & 0 + 1 = 1 ) ) ;

per cases ( k = 0 or ( 1 <= k & k <= len w1 ) ) by A3, A4, NAT_1:13;

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

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

end;

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

len w1 <= (len w1) + (len w2) by NAT_1:11;
then k <= (len w1) + (len w2) by A6, XXREAL_0:2;
then k <= len (w1 ^ w2) by FINSEQ_1:22;
then A7: ex wk being Element of IAlph ex qwk, qwk1 being State of fsm st
( wk = (w1 ^ w2) . k & qwk = ((q1,(w1 ^ w2)) -admissible) . k & qwk1 = ((q1,(w1 ^ w2)) -admissible) . (k + 1) & wk -succ_of qwk = qwk1 ) by A6, Def2;
( ex w1k being Element of IAlph ex qw1k, qw1k1 being State of fsm st
( w1k = w1 . k & qw1k = ((q1,w1) -admissible) . k & qw1k1 = ((q1,w1) -admissible) . (k + 1) & w1k -succ_of qw1k = qw1k1 ) & k in dom w1 ) by A6, Def2, FINSEQ_3:25;
hence ((q1,(w1 ^ w2)) -admissible) . (k + 1) = ((q1,w1) -admissible) . (k + 1) by A2, A6, A7, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

end;

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