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;
set fg = f ^ g;
set iL = i + (len f);
set Dfg = Del (f ^ g),(i + (len f));
set fD = f ^ (Del g,i);
consider m being Nat such that
A2: ( len g = m + 1 & len (Del g,i) = m ) by A1, FINSEQ_3:113;
A3: ( len (f ^ g) = (len f) + (len g) & len (f ^ (Del g,i)) = (len f) + (len (Del g,i)) ) by FINSEQ_1:35;
i in Seg (len g) by A1, FINSEQ_1:def 3;
then A4: ( i + (len f) in Seg (len (f ^ g)) & dom (f ^ g) = Seg (len (f ^ g)) & i > 0 ) by A3, FINSEQ_1:3, FINSEQ_1:81, FINSEQ_1:def 3;
A5: len (f ^ g) = (m + (len f)) + 1 by A2, A3;
then A6: len (Del (f ^ g),(i + (len f))) = m + (len f) by A4, FINSEQ_3:118;

now

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 A7: ( 1 <= j & j <= m + (len f) ) ; :: thesis: (f ^ (Del g,i)) . j = (Del (f ^ g),(i + (len f))) . j

now

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

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

0 + (len f) < i + (len f) by A4, XREAL_1:10;
then A9: ( j < i + (len f) & j in dom f ) by A7, A8, FINSEQ_3:27, XXREAL_0:2;
hence (Del (f ^ g),(i + (len f))) . j = (f ^ g) . j by A5, FINSEQ_3:119
.= f . j by A9, FINSEQ_1:def 7
.= (f ^ (Del g,i)) . j by A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A10: 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;
jL <> 0 by A10;
then A11: jL >= 1 by NAT_1:14;
jL + (len f) <= m + (len f) by A7;
then A12: jL <= m by XREAL_1:8;
then A13: ( jL in dom (Del g,i) & jL <= len g & 1 <= jL + 1 & jL + 1 <= len g ) by A2, A11, FINSEQ_3:27, NAT_1:13, XREAL_1:9;
then A14: ( jL in dom g & jL + 1 in dom g ) by A11, FINSEQ_3:27;

now

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

suppose A15: 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:10;
hence (Del (f ^ g),(i + (len f))) . j = (f ^ g) . (jL + (len f)) by A5, FINSEQ_3:119
.= g . jL by A14, FINSEQ_1:def 7
.= (Del g,i) . jL by A1, A2, A15, FINSEQ_3:119
.= (f ^ (Del g,i)) . (jL + (len f)) by A13, FINSEQ_1:def 7
.= (f ^ (Del g,i)) . j ;
:: thesis: verum

end;

suppose A16: 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:9;
hence (Del (f ^ g),(i + (len f))) . j = (f ^ g) . ((jL + (len f)) + 1) by A4, A5, A7, FINSEQ_3:120
.= (f ^ g) . ((jL + 1) + (len f))
.= g . (jL + 1) by A14, FINSEQ_1:def 7
.= (Del g,i) . jL by A1, A2, A12, A16, FINSEQ_3:120
.= (f ^ (Del g,i)) . (jL + (len f)) by A13, 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;

hence Del (f ^ g),(i + (len f)) = f ^ (Del g,i) by A2, A3, A6, FINSEQ_1:18; :: thesis: verum