let i be Nat; :: thesis: for D being non empty set
for f, g being FinSequence of D st i in dom g holds
Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i))
let D be non empty set ; :: thesis: for f, g being FinSequence of D st i in dom g holds
Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i))
let f, g be FinSequence of D; :: thesis: ( i in dom g implies Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i)) )
assume A1: i in dom g ; :: thesis: Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i))
set Dg = Del (g,i);
consider m being Nat such that
A2: len g = m + 1 and
A3: len (Del (g,i)) = m by A1, FINSEQ_3:104;
set fD = f ^ (Del (g,i));
set iL = i + (len f);
set fg = f ^ g;
set Dfg = Del ((f ^ g),(i + (len f)));
A4: dom (f ^ g) = Seg (len (f ^ g)) by FINSEQ_1:def 3;
A5: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A6: len (f ^ g) = (m + (len f)) + 1 by A2;
A7: i in Seg (len g) by A1, FINSEQ_1:def 3;
then A8: i > 0 ;

A9: now :: thesis: for j being Nat st 1 <= j & j <= m + (len f) holds
(f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j

let j be Nat; :: thesis: ( 1 <= j & j <= m + (len f) implies (f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j )
assume that
A10: 1 <= j and
A11: j <= m + (len f) ; :: thesis: (f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j

now :: thesis: (Del ((f ^ g),(i + (len f)))) . j = (f ^ (Del (g,i))) . j

per cases ( j <= len f or j > len f ) ;

suppose A12: j <= len f ; :: thesis: (Del ((f ^ g),(i + (len f)))) . j = (f ^ (Del (g,i))) . j

then A13: j in dom f by A10, FINSEQ_3:25;
0 + (len f) < i + (len f) by A8, XREAL_1:8;
then j < i + (len f) by A12, XXREAL_0:2;
hence (Del ((f ^ g),(i + (len f)))) . j = (f ^ g) . j by FINSEQ_3:110
.= f . j by A13, FINSEQ_1:def 7
.= (f ^ (Del (g,i))) . j by A13, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A14: j > len f ; :: thesis: (f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j

then reconsider jL = j - (len f) as Element of NAT by NAT_1:21;
A15: 1 <= jL + 1 by NAT_1:14;
jL + (len f) <= m + (len f) by A11;
then A16: jL <= m by XREAL_1:6;
then jL + 1 <= len g by A2, XREAL_1:7;
then A17: jL + 1 in dom g by A15, FINSEQ_3:25;
jL <> 0 by A14;
then A18: jL >= 1 by NAT_1:14;
then A19: jL in dom (Del (g,i)) by A3, A16, FINSEQ_3:25;
jL <= len g by A2, A16, NAT_1:13;
then A20: jL in dom g by A18, FINSEQ_3:25;

now :: thesis: (Del ((f ^ g),(i + (len f)))) . j = (f ^ (Del (g,i))) . j

per cases ( jL < i or jL >= i ) ;

suppose A21: jL < i ; :: thesis: (Del ((f ^ g),(i + (len f)))) . j = (f ^ (Del (g,i))) . j

then jL + (len f) < i + (len f) by XREAL_1:8;
hence (Del ((f ^ g),(i + (len f)))) . j = (f ^ g) . (jL + (len f)) by FINSEQ_3:110
.= g . jL by A20, FINSEQ_1:def 7
.= (Del (g,i)) . jL by A21, FINSEQ_3:110
.= (f ^ (Del (g,i))) . (jL + (len f)) by A19, FINSEQ_1:def 7
.= (f ^ (Del (g,i))) . j ;
:: thesis: verum

end;

suppose A22: jL >= i ; :: thesis: (Del ((f ^ g),(i + (len f)))) . j = (f ^ (Del (g,i))) . j

then jL + (len f) >= i + (len f) by XREAL_1:7;
hence (Del ((f ^ g),(i + (len f)))) . j = (f ^ g) . ((jL + (len f)) + 1) by A5, A7, A4, A6, A11, FINSEQ_1:60, FINSEQ_3:111
.= (f ^ g) . ((jL + 1) + (len f))
.= g . (jL + 1) by A17, FINSEQ_1:def 7
.= (Del (g,i)) . jL by A1, A2, A16, A22, FINSEQ_3:111
.= (f ^ (Del (g,i))) . (jL + (len f)) by A19, FINSEQ_1:def 7
.= (f ^ (Del (g,i))) . j ;
:: thesis: verum

end;

end;

end;

hence (f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j ; :: thesis: verum

end;

end;

end;

hence (f ^ (Del (g,i))) . j = (Del ((f ^ g),(i + (len f)))) . j ; :: thesis: verum

end;

A23: len (f ^ (Del (g,i))) = (len f) + (len (Del (g,i))) by FINSEQ_1:22;
len (Del ((f ^ g),(i + (len f)))) = m + (len f) by A5, A7, A4, A6, FINSEQ_1:60, FINSEQ_3:109;
hence Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i)) by A3, A23, A9; :: thesis: verum