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);
consider m being Nat such that
A2: len f = m + 1 and
A3: len (Del (f,i)) = m by A1, FINSEQ_3:104;
set Dg = (Del (f,i)) ^ g;
set fg = f ^ g;
set Dfg = Del ((f ^ g),i);
A4: Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def 3;
A5: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len f <= len (f ^ g) by NAT_1:12;
then A6: Seg (len f) c= Seg (len (f ^ g)) by FINSEQ_1:5;
A7: len (f ^ g) = ((len g) + m) + 1 by A2, A5;
A8: Seg (len f) = dom f by FINSEQ_1:def 3;

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

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

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

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

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

i <= len f by A1, FINSEQ_3:25;
then A13: j < len f by A12, XXREAL_0:2;
then A14: j in dom f by A10, FINSEQ_3:25;
j <= m by A2, A13, NAT_1:13;
then A15: j in dom (Del (f,i)) by A3, A10, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j = (f ^ g) . j by A12, FINSEQ_3:110
.= f . j by A14, FINSEQ_1:def 7
.= (Del (f,i)) . j by A12, FINSEQ_3:110
.= ((Del (f,i)) ^ g) . j by A15, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

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

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

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

A18: 0 + 1 <= j + 1 by XREAL_1:7;
j + 1 <= len f by A2, A17, XREAL_1:7;
then A19: j + 1 in dom f by A18, FINSEQ_3:25;
A20: j in dom (Del (f,i)) by A3, A10, A17, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j = (f ^ g) . (j + 1) by A1, A6, A8, A4, A7, A11, A16, FINSEQ_3:111
.= f . (j + 1) by A19, FINSEQ_1:def 7
.= (Del (f,i)) . j by A1, A2, A16, A17, FINSEQ_3:111
.= ((Del (f,i)) ^ g) . j by A20, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A21: 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 A11, XREAL_1:7;
then jL + (len f) <= (len f) + (len g) by A2;
then A22: jL <= len g by XREAL_1:8;
jL <> 0 by A2, A21;
then jL >= 1 by NAT_1:14;
then A23: jL in dom g by A22, FINSEQ_3:25;
thus (Del ((f ^ g),i)) . j = (f ^ g) . (jL + (len f)) by A1, A6, A8, A4, A7, A11, A16, FINSEQ_3:111
.= g . jL by A23, FINSEQ_1:def 7
.= ((Del (f,i)) ^ g) . (m + jL) by A3, A23, 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;

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