let IAlph, OAlph be non empty set ; :: thesis: for s being Element of IAlph
for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
let s be Element of IAlph; :: thesis: for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
let w be FinSequence of IAlph; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
let qa, qa9 be State of tfsm; :: thesis: ( qa9 = the Tran of tfsm . [qa,s] implies for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i )
set sw = <*s*> ^ w;
A1: len (<*s*> ^ w) = (len <*s*>) + (len w) by FINSEQ_1:22
.= (len w) + 1 by FINSEQ_1:40 ;
defpred S₁[ Nat] means ( $1 in Seg ((len w) + 1) implies ((qa,(<*s*> ^ w)) -admissible) . ($1 + 1) = ((qa9,w) -admissible) . $1 );
A2: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;
assume A3: qa9 = the Tran of tfsm . [qa,s] ; :: thesis: for i being Nat st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
A4: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A5: ( j in Seg ((len w) + 1) implies ((qa,(<*s*> ^ w)) -admissible) . (j + 1) = ((qa9,w) -admissible) . j ) ; :: thesis: S₁[j + 1]
assume A6: j + 1 in Seg ((len w) + 1) ; :: thesis: ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) = ((qa9,w) -admissible) . (j + 1)

per cases ( j = 0 or j <> 0 ) ;

suppose A7: j = 0 ; :: thesis: ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) = ((qa9,w) -admissible) . (j + 1)

set aadm = (qa,(<*s*> ^ w)) -admissible ;
1 <= len (<*s*> ^ w) by A1, A6, A7, FINSEQ_1:1;
then A8: ex swi1 being Element of IAlph ex a1, a11 being Element of tfsm st
( swi1 = (<*s*> ^ w) . 1 & a1 = ((qa,(<*s*> ^ w)) -admissible) . 1 & a11 = ((qa,(<*s*> ^ w)) -admissible) . (1 + 1) & swi1 -succ_of a1 = a11 ) by Def2;
((qa9,w) -admissible) . 1 = qa9 by Def2;
hence ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) = ((qa9,w) -admissible) . (j + 1) by A3, A2, A7, A8, Def2; :: thesis: verum

end;

suppose A9: j <> 0 ; :: thesis: ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) = ((qa9,w) -admissible) . (j + 1)

set aadm = (qa,(<*s*> ^ w)) -admissible ;
set aadm9 = (qa9,w) -admissible ;
A10: j in Seg (len w) by A6, A9, FINSEQ_1:61;
then A11: j <= len w by FINSEQ_1:1;
then ( 1 <= j + 1 & j + 1 <= len (<*s*> ^ w) ) by A1, NAT_1:12, XREAL_1:7;
then A12: ex swj1 being Element of IAlph ex aj1, aj11 being Element of tfsm st
( swj1 = (<*s*> ^ w) . (j + 1) & aj1 = ((qa,(<*s*> ^ w)) -admissible) . (j + 1) & aj11 = ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) & swj1 -succ_of aj1 = aj11 ) by Def2;
1 <= j by A10, FINSEQ_1:1;
then A13: ex wj being Element of IAlph ex aj9, aj19 being Element of tfsm st
( wj = w . j & aj9 = ((qa9,w) -admissible) . j & aj19 = ((qa9,w) -admissible) . (j + 1) & wj -succ_of aj9 = aj19 ) by A11, Def2;
j in dom w by A10, FINSEQ_1:def 3;
hence ((qa,(<*s*> ^ w)) -admissible) . ((j + 1) + 1) = ((qa9,w) -admissible) . (j + 1) by A5, A6, A9, A12, A13, FINSEQ_1:61, FINSEQ_3:103; :: thesis: verum

end;

end;

end;

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