let IAlph, OAlph be non empty set ; :: thesis: for w1, w2 being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let w1, w2 be FinSequence of IAlph; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let q1t, q2t be State of tfsm; :: thesis: ( q1t,w1 -leads_to q2t implies (q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response) )
set q1w1 = (q1t,w1) -response ;
set q2w2 = (q2t,w2) -response ;
set q1w1w2 = (q1t,(w1 ^ w2)) -response ;
set Dq1w1w2a = Del (((q1t,w1) -admissible),((len w1) + 1));
set OF = the OFun of tfsm;
assume A1: q1t,w1 -leads_to q2t ; :: thesis: (q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)

A2: now :: thesis: for k being Nat st 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) holds
((q1t,(w1 ^ w2)) -response) . k = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k

dom ((q1t,w1) -admissible) = Seg (len ((q1t,w1) -admissible)) by FINSEQ_1:def 3;
then dom ((q1t,w1) -admissible) = Seg ((len w1) + 1) by Def2;
then (len w1) + 1 in dom ((q1t,w1) -admissible) by FINSEQ_1:3;
then consider m being Nat such that
A3: len ((q1t,w1) -admissible) = m + 1 and
A4: len (Del (((q1t,w1) -admissible),((len w1) + 1))) = m by FINSEQ_3:104;
A5: m + 1 = (len w1) + 1 by A3, Def2;
A6: len ((q1t,w1) -response) = len w1 by Def6;
let k be Nat; :: thesis: ( 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) implies ((q1t,(w1 ^ w2)) -response) . b₁ = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b₁ )
assume that
A7: 1 <= k and
A8: k <= len ((q1t,(w1 ^ w2)) -response) ; :: thesis: ((q1t,(w1 ^ w2)) -response) . b₁ = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b₁

per cases ( ( 1 <= k & k <= len ((q1t,w1) -response) ) or ( (len ((q1t,w1) -response)) + 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) ) ) by A7, A8, NAT_1:13;

suppose A9: ( 1 <= k & k <= len ((q1t,w1) -response) ) ; :: thesis: ((q1t,(w1 ^ w2)) -response) . b₁ = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b₁

then A10: k <= len w1 by Def6;
then A11: k in dom w1 by A9, FINSEQ_3:25;
A12: k in dom (Del (((q1t,w1) -admissible),((len w1) + 1))) by A4, A5, A9, A10, FINSEQ_3:25;
A13: k < (len w1) + 1 by A10, NAT_1:13;
A14: k in dom ((q1t,w1) -response) by A9, FINSEQ_3:25;
k <= len (w1 ^ w2) by A8, Def6;
then k in dom (w1 ^ w2) by A7, FINSEQ_3:25;
hence ((q1t,(w1 ^ w2)) -response) . k = the OFun of tfsm . [(((q1t,(w1 ^ w2)) -admissible) . k),((w1 ^ w2) . k)] by Def6
.= the OFun of tfsm . [(((Del (((q1t,w1) -admissible),((len w1) + 1))) ^ ((q2t,w2) -admissible)) . k),((w1 ^ w2) . k)] by A1, Th8
.= the OFun of tfsm . [((Del (((q1t,w1) -admissible),((len w1) + 1))) . k),((w1 ^ w2) . k)] by A12, FINSEQ_1:def 7
.= the OFun of tfsm . [((Del (((q1t,w1) -admissible),((len w1) + 1))) . k),(w1 . k)] by A11, FINSEQ_1:def 7
.= the OFun of tfsm . [(((q1t,w1) -admissible) . k),(w1 . k)] by A13, FINSEQ_3:110
.= ((q1t,w1) -response) . k by A11, Def6
.= (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k by A14, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A15: ( (len ((q1t,w1) -response)) + 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) ) ; :: thesis: ((q1t,(w1 ^ w2)) -response) . b₁ = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b₁

then A16: ((len ((q1t,w1) -response)) + 1) - (len ((q1t,w1) -response)) <= k - (len ((q1t,w1) -response)) by XREAL_1:9;
then reconsider p = k - (len ((q1t,w1) -response)) as Element of NAT by INT_1:3;
A17: len ((q1t,(w1 ^ w2)) -response) = len (w1 ^ w2) by Def6
.= (len w1) + (len w2) by FINSEQ_1:22 ;
then k <= (len ((q1t,w1) -response)) + (len w2) by A15, Def6;
then k - (len ((q1t,w1) -response)) <= ((len ((q1t,w1) -response)) + (len w2)) - (len ((q1t,w1) -response)) by XREAL_1:9;
then A18: p in dom w2 by A16, FINSEQ_3:25;
A19: (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + 1 <= k by A4, A5, A15, Def6;
A20: (len w1) + 1 <= k by A15, Def6;
A21: len ((q1t,(w1 ^ w2)) -response) = len (w1 ^ w2) by Def6
.= (len w1) + (len w2) by FINSEQ_1:22
.= (len ((q1t,w1) -response)) + (len w2) by Def6
.= (len ((q1t,w1) -response)) + (len ((q2t,w2) -response)) by Def6 ;
then A22: (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k = ((q2t,w2) -response) . p by A15, FINSEQ_1:23
.= the OFun of tfsm . [(((q2t,w2) -admissible) . p),(w2 . p)] by A18, Def6
.= the OFun of tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len ((q1t,w1) -response))))] by Def6
.= the OFun of tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len w1)))] by Def6 ;
len w2 <= (len w2) + 1 by NAT_1:11;
then A23: (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len w2) <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + ((len w2) + 1) by XREAL_1:6;
k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len w2) by A4, A5, A6, A15, A21, Def6;
then k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + ((len w2) + 1) by A23, XXREAL_0:2;
then A24: k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len ((q2t,w2) -admissible)) by Def2;
k <= len (w1 ^ w2) by A8, Def6;
then k in dom (w1 ^ w2) by A7, FINSEQ_3:25;
then ((q1t,(w1 ^ w2)) -response) . k = the OFun of tfsm . [(((q1t,(w1 ^ w2)) -admissible) . k),((w1 ^ w2) . k)] by Def6
.= the OFun of tfsm . [(((Del (((q1t,w1) -admissible),((len w1) + 1))) ^ ((q2t,w2) -admissible)) . k),((w1 ^ w2) . k)] by A1, Th8
.= the OFun of tfsm . [(((q2t,w2) -admissible) . (k - (len (Del (((q1t,w1) -admissible),((len w1) + 1)))))),((w1 ^ w2) . k)] by A19, A24, FINSEQ_1:23
.= the OFun of tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len w1)))] by A4, A5, A15, A17, A20, FINSEQ_1:23 ;
hence ((q1t,(w1 ^ w2)) -response) . k = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k by A22; :: thesis: verum

end;

end;

end;

len ((q1t,(w1 ^ w2)) -response) = len (w1 ^ w2) by Def6
.= (len w1) + (len w2) by FINSEQ_1:22
.= (len ((q1t,w1) -response)) + (len w2) by Def6
.= (len ((q1t,w1) -response)) + (len ((q2t,w2) -response)) by Def6
.= len (((q1t,w1) -response) ^ ((q2t,w2) -response)) by FINSEQ_1:22 ;
hence (q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response) by A2, FINSEQ_1:14; :: thesis: verum