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
(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 over IAlph,OAlph
for qa, qa9 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 over IAlph,OAlph
for qa, qa9 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 over IAlph,OAlph; :: thesis: for qa, qa9 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 qa, qa9 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:22
.= 1 + (len w) by FINSEQ_1:40 ;
assume A2: qa9 = the Tran of tfsm . [qa,s] ; :: thesis: (qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)

now :: thesis: ( len ((qa,(<*s*> ^ w)) -response) = 1 + (len w) & 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) . j = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j ) )

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:22
.= 1 + (len ((qa9,w) -response)) by FINSEQ_1:40
.= 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:1;
A7: j <= 1 + (len w) by A3, A5, FINSEQ_1:1;
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:41
.= (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j by A9, FINSEQ_1:41 ; :: 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:51;
j <= (len w) + 1 by A3, A5, FINSEQ_1:1;
then j - 1 <= ((len w) + 1) - 1 by XREAL_1:9;
then A13: i in Seg (len w) by A11, A12, FINSEQ_1:1;
then A14: i in Seg (1 + (len w)) by FINSEQ_2:8;
i + 1 in Seg (1 + (len w)) by A13, FINSEQ_1:60;
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:40;
then (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j = ((qa9,w) -response) . i by A4, A7, A10, A11, FINSEQ_1:24
.= 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:103
.= the OFun of tfsm . [(((qa,(<*s*> ^ w)) -admissible) . (i + 1)),((<*s*> ^ w) . (i + 1))] by A2, A14, Th17
.= ((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:9; :: thesis: verum