let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over 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 = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
let fsm be non empty FSM over 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 = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
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 = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
let q1, q2 be State of fsm; :: thesis: ( q1,w1 -leads_to q2 implies (q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible) )
set q1w = (q1,(w1 ^ w2)) -admissible ;
set q1w1 = (q1,w1) -admissible ;
set q2w2 = (q2,w2) -admissible ;
set Dw1 = Del (((q1,w1) -admissible),((len w1) + 1));
A1: len ((q1,w1) -admissible) = (len w1) + 1 by Def2;
( len ((q1,w1) -admissible) = (len w1) + 1 & dom ((q1,w1) -admissible) = Seg (len ((q1,w1) -admissible)) ) by Def2, FINSEQ_1:def 3;
then (len w1) + 1 in dom ((q1,w1) -admissible) by FINSEQ_1:3;
then A2: ex m being Nat st
( len ((q1,w1) -admissible) = m + 1 & len (Del (((q1,w1) -admissible),((len w1) + 1))) = m ) by FINSEQ_3:104;
A3: len ((q1,(w1 ^ w2)) -admissible) = (len (w1 ^ w2)) + 1 by Def2
.= ((len w1) + (len w2)) + 1 by FINSEQ_1:22
.= (len (Del (((q1,w1) -admissible),((len w1) + 1)))) + ((len w2) + 1) by A2, A1
.= (len (Del (((q1,w1) -admissible),((len w1) + 1)))) + (len ((q2,w2) -admissible)) by Def2
.= len ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) by FINSEQ_1:22 ;
assume A4: q1,w1 -leads_to q2 ; :: thesis: (q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)

now :: thesis: for k being Nat st 1 <= k & k <= len ((q1,(w1 ^ w2)) -admissible) holds
((q1,(w1 ^ w2)) -admissible) . k = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len ((q1,(w1 ^ w2)) -admissible) implies ((q1,(w1 ^ w2)) -admissible) . b₁ = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b₁ )
assume A5: ( 1 <= k & k <= len ((q1,(w1 ^ w2)) -admissible) ) ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . b₁ = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b₁

per cases ( ( 1 <= k & k <= len w1 ) or ( (len w1) + 1 <= k & k <= len ((q1,(w1 ^ w2)) -admissible) ) ) by A5, NAT_1:13;

suppose A6: ( 1 <= k & k <= len w1 ) ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . b₁ = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b₁

then A7: k < (len w1) + 1 by NAT_1:13;
A8: k in dom (Del (((q1,w1) -admissible),((len w1) + 1))) by A2, A1, A6, FINSEQ_3:25;
thus ((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k by A6, Th5
.= (Del (((q1,w1) -admissible),((len w1) + 1))) . k by A7, FINSEQ_3:110
.= ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k by A8, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A9: ( (len w1) + 1 <= k & k <= len ((q1,(w1 ^ w2)) -admissible) ) ; :: thesis: ((q1,(w1 ^ w2)) -admissible) . b₁ = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b₁

then k <= (len (Del (((q1,w1) -admissible),((len w1) + 1)))) + (len ((q2,w2) -admissible)) by A3, FINSEQ_1:22;
then A10: ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k = ((q2,w2) -admissible) . (k - (len w1)) by A2, A1, A9, FINSEQ_1:23;
((len w1) + 1) - (len w1) <= k - (len w1) by A9, XREAL_1:9;
then reconsider i = k - (len w1) as Element of NAT by INT_1:3;
A11: k = (len w1) + i ;
len ((q1,(w1 ^ w2)) -admissible) = (len (w1 ^ w2)) + 1 by Def2;
then k <= ((len w1) + (len w2)) + 1 by A9, FINSEQ_1:22;
then k <= (len w1) + ((len w2) + 1) ;
then A12: i <= (len w2) + 1 by A11, XREAL_1:6;
1 <= i by A9, A11, XREAL_1:6;
hence ((q1,(w1 ^ w2)) -admissible) . k = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k by A4, A11, A12, A10, Th7; :: thesis: verum

end;

end;

end;

hence (q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible) by A3, FINSEQ_1:14; :: thesis: verum