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 of IAlph,OAlph
for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )
let s be Element of IAlph; :: thesis: for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )
let w be FinSequence of IAlph; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )
let qa9, qa be State of tfsm; :: thesis: ( qa9 = the Tran of tfsm . [qa,s] implies qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response ) )
set OF = the OFun of tfsm;
set asresp = the OFun of tfsm . [qa,s];
A1: len (<*s*> ^ w) = (len <*s*>) + (len w) by FINSEQ_1:35
.= 1 + (len w) by FINSEQ_1:57 ;
assume A2: qa9 = the Tran of tfsm . [qa,s] ; :: thesis: qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )

now

thus len (qa,(<*s*> ^ w) -response ) = 1 + (len w) by A1, Def6; :: thesis: ( len (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) = 1 + (len w) & ( for j being Nat st j in dom (qa,(<*s*> ^ w) -response ) holds
(qa,(<*s*> ^ w) -response ) . b₂ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₂ ) )
then A3: dom (qa,(<*s*> ^ w) -response ) = Seg (1 + (len w)) by FINSEQ_1:def 3;
thus A4: len (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) = (len <*(the OFun of tfsm . [qa,s])*>) + (len (qa9,w -response )) by FINSEQ_1:35
.= 1 + (len (qa9,w -response )) by FINSEQ_1:57
.= 1 + (len w) by Def6 ; :: thesis: for j being Nat st j in dom (qa,(<*s*> ^ w) -response ) holds
(qa,(<*s*> ^ w) -response ) . b₂ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₂
let j be Nat; :: thesis: ( j in dom (qa,(<*s*> ^ w) -response ) implies (qa,(<*s*> ^ w) -response ) . b₁ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₁ )
assume A5: j in dom (qa,(<*s*> ^ w) -response ) ; :: thesis: (qa,(<*s*> ^ w) -response ) . b₁ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₁
then A6: 1 <= j by A3, FINSEQ_1:3;
A7: j <= 1 + (len w) by A3, A5, FINSEQ_1:3;
A8: j in dom (<*s*> ^ w) by A1, A3, A5, FINSEQ_1:def 3;

per cases ( j = 1 or j > 1 ) by A6, XXREAL_0:1;

suppose A9: j = 1 ; :: thesis: (qa,(<*s*> ^ w) -response ) . b₁ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₁

thus (qa,(<*s*> ^ w) -response ) . j = the OFun of tfsm . [((qa,(<*s*> ^ w) -admissible ) . j),((<*s*> ^ w) . j)] by A8, Def6
.= the OFun of tfsm . [qa,((<*s*> ^ w) . j)] by A9, Def2
.= the OFun of tfsm . [qa,s] by A9, FINSEQ_1:58
.= (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . j by A9, FINSEQ_1:58 ; :: thesis: verum

end;

suppose A10: j > 1 ; :: thesis: (qa,(<*s*> ^ w) -response ) . b₁ = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . b₁

then consider i being Element of NAT such that
A11: i = j - 1 and
A12: 1 <= i by INT_1:78;
j <= (len w) + 1 by A3, A5, FINSEQ_1:3;
then j - 1 <= ((len w) + 1) - 1 by XREAL_1:11;
then A13: i in Seg (len w) by A11, A12, FINSEQ_1:3;
then A14: i in Seg (1 + (len w)) by FINSEQ_2:9;
i + 1 in Seg (1 + (len w)) by A13, FINSEQ_1:81;
then A15: i + 1 in dom (<*s*> ^ w) by A1, FINSEQ_1:def 3;
A16: i in dom w by A13, FINSEQ_1:def 3;
len <*(the OFun of tfsm . [qa,s])*> = 1 by FINSEQ_1:57;
then (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . j = (qa9,w -response ) . i by A4, A7, A10, A11, FINSEQ_1:37
.= the OFun of tfsm . [((qa9,w -admissible ) . i),(w . i)] by A16, Def6
.= the OFun of tfsm . [((qa9,w -admissible ) . i),((<*s*> ^ w) . (i + 1))] by A16, FINSEQ_3:112
.= the OFun of tfsm . [((qa,(<*s*> ^ w) -admissible ) . (i + 1)),((<*s*> ^ w) . (i + 1))] by A2, A14, Th34
.= (qa,(<*s*> ^ w) -response ) . j by A11, A15, Def6 ;
hence (qa,(<*s*> ^ w) -response ) . j = (<*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response )) . j ; :: thesis: verum

end;

end;

end;

hence qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa9,w -response ) by FINSEQ_2:10; :: thesis: verum