let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
let fsm be non empty FSM of IAlph; :: thesis: for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
let w1, w2 be FinSequence of IAlph; :: thesis: for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
let q1, q2 be State of fsm; :: thesis: ( q1,w1 -leads_to q2 implies ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2 )
assume A1: q1,w1 -leads_to q2 ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
set q1w1 = (q1,w1) -admissible ;
set q1w = (q1,(w1 ^ w2)) -admissible ;

per cases ( len w1 = 0 or len w1 > 0 ) ;

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

( ((q1,w1) -admissible) . 1 = q1 & ((q1,w1) -admissible) . ((len w1) + 1) = q2 ) by A1, Def2, Def3;
hence ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2 by A2, Def2; :: thesis: verum

end;

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

A4: len ((q1,w1) -admissible) = (len w1) + 1 by Def2;
0 + 1 = 1 ;
then A5: 1 <= len w1 by A3, NAT_1:13;
then consider w1k being Element of IAlph, qw1k, qw1k1 being State of fsm such that
A6: w1k = w1 . (len w1) and
A7: qw1k = ((q1,w1) -admissible) . (len w1) and
A8: qw1k1 = ((q1,w1) -admissible) . ((len w1) + 1) and
A9: w1k -succ_of qw1k = qw1k1 by Def2;
len (w1 ^ w2) = (len w1) + (len w2) by FINSEQ_1:22;
then len w1 <= len (w1 ^ w2) by NAT_1:12;
then consider wk being Element of IAlph, qwk, qwk1 being State of fsm such that
A10: wk = (w1 ^ w2) . (len w1) and
A11: ( qwk = ((q1,(w1 ^ w2)) -admissible) . (len w1) & qwk1 = ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) & wk -succ_of qwk = qwk1 ) by A5, Def2;
len w1 in Seg (len w1) by A3, FINSEQ_1:3;
then len w1 in dom w1 by FINSEQ_1:def 3;
then wk = w1k by A10, A6, FINSEQ_1:def 7;
hence ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = qw1k1 by A5, A11, A7, A9, Th20
.= q2 by A1, A8, A4, Th19 ;
:: thesis: verum

end;

end;