let i be Nat; :: thesis: for D being non empty set
for f, g being FinSequence of D st i in dom f holds
Del (f ^ g),i = (Del f,i) ^ g
let D be non empty set ; :: thesis: for f, g being FinSequence of D st i in dom f holds
Del (f ^ g),i = (Del f,i) ^ g
let f, g be FinSequence of D; :: thesis: ( i in dom f implies Del (f ^ g),i = (Del f,i) ^ g )
assume A1: i in dom f ; :: thesis: Del (f ^ g),i = (Del f,i) ^ g
set Df = Del f,i;
set fg = f ^ g;
set Dfg = Del (f ^ g),i;
set Dg = (Del f,i) ^ g;
consider m being Nat such that
A2: ( len f = m + 1 & len (Del f,i) = m ) by A1, FINSEQ_3:113;
A3: ( len (f ^ g) = (len f) + (len g) & len ((Del f,i) ^ g) = (len (Del f,i)) + (len g) ) by FINSEQ_1:35;
then len f <= len (f ^ g) by NAT_1:12;
then A4: ( Seg (len f) c= Seg (len (f ^ g)) & Seg (len f) = dom f & Seg (len (f ^ g)) = dom (f ^ g) ) by FINSEQ_1:7, FINSEQ_1:def 3;
A5: len (f ^ g) = ((len g) + m) + 1 by A2, A3;
then A6: len (Del (f ^ g),i) = m + (len g) by A1, A4, FINSEQ_3:118;

now

let j be Nat; :: thesis: ( 1 <= j & j <= m + (len g) implies ((Del f,i) ^ g) . j = (Del (f ^ g),i) . j )
assume A7: ( 1 <= j & j <= m + (len g) ) ; :: thesis: ((Del f,i) ^ g) . j = (Del (f ^ g),i) . j
A8: ( i in NAT & j in NAT ) by ORDINAL1:def 13;

now

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

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

i <= len f by A1, FINSEQ_3:27;
then j < len f by A9, XXREAL_0:2;
then A10: ( j in dom f & j <= m ) by A2, A7, FINSEQ_3:27, NAT_1:13;
then A11: j in dom (Del f,i) by A2, A7, FINSEQ_3:27;
thus (Del (f ^ g),i) . j = (f ^ g) . j by A5, A8, A9, FINSEQ_3:119
.= f . j by A10, FINSEQ_1:def 7
.= (Del f,i) . j by A2, A8, A9, FINSEQ_3:119
.= ((Del f,i) ^ g) . j by A11, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

now

per cases ( j <= m or j > m ) ;

suppose A13: j <= m ; :: thesis: (Del (f ^ g),i) . j = ((Del f,i) ^ g) . j

then ( 0 + 1 <= j + 1 & j + 1 <= len f ) by A2, XREAL_1:9;
then A14: ( j + 1 in dom f & j in dom (Del f,i) ) by A2, A7, A13, FINSEQ_3:27;
thus (Del (f ^ g),i) . j = (f ^ g) . (j + 1) by A1, A4, A5, A7, A12, A8, FINSEQ_3:120
.= f . (j + 1) by A14, FINSEQ_1:def 7
.= (Del f,i) . j by A8, A1, A2, A12, A13, FINSEQ_3:120
.= ((Del f,i) ^ g) . j by A14, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A15: j > m ; :: thesis: (Del (f ^ g),i) . j = ((Del f,i) ^ g) . j

then j >= len f by A2, NAT_1:13;
then j + 1 > len f by NAT_1:13;
then reconsider jL = (j + 1) - (len f) as Element of NAT by NAT_1:21;
j + 1 <= (m + (len g)) + 1 by A7, XREAL_1:9;
then jL + (len f) <= (len f) + (len g) by A2;
then A16: jL <= len g by XREAL_1:10;
jL <> 0 by A2, A15;
then jL >= 1 by NAT_1:14;
then A17: jL in dom g by A16, FINSEQ_3:27;
thus (Del (f ^ g),i) . j = (f ^ g) . (jL + (len f)) by A1, A4, A5, A7, A12, A8, FINSEQ_3:120
.= g . jL by A17, FINSEQ_1:def 7
.= ((Del f,i) ^ g) . (m + jL) by A2, A17, FINSEQ_1:def 7
.= ((Del f,i) ^ g) . j by A2 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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