let i be Nat; :: thesis: for a being set
for p, q being FinSequence st p +* (i,a) = q +* (i,a) holds
Del (p,i) = Del (q,i)
let a be set ; :: thesis: for p, q being FinSequence st p +* (i,a) = q +* (i,a) holds
Del (p,i) = Del (q,i)
let p, q be FinSequence; :: thesis: ( p +* (i,a) = q +* (i,a) implies Del (p,i) = Del (q,i) )
set x = p;
set y = q;
assume A1: p +* (i,a) = q +* (i,a) ; :: thesis: Del (p,i) = Del (q,i)
set xi = p +* (i,a);
set yi = q +* (i,a);
set dx = Del (p,i);
set dy = Del (q,i);
A2: dom (p +* (i,a)) = dom p by FUNCT_7:30;
A3: dom (q +* (i,a)) = dom q by FUNCT_7:30;
A4: Seg (len q) = dom q by FINSEQ_1:def 3;
A5: Seg (len p) = dom p by FINSEQ_1:def 3;

per cases ( i in dom p or not i in dom p ) ;

suppose A6: i in dom p ; :: thesis: Del (p,i) = Del (q,i)

A7: dom (Del (p,i)) = Seg (len (Del (p,i))) by FINSEQ_1:def 3;

now :: thesis: ( len (Del (p,i)) = len (Del (p,i)) & len (Del (q,i)) = len (Del (p,i)) & ( for j being Nat st j in dom (Del (p,i)) holds
(Del (p,i)) . j = (Del (q,i)) . j ) )

thus len (Del (p,i)) = len (Del (p,i)) ; :: thesis: ( len (Del (q,i)) = len (Del (p,i)) & ( for j being Nat st j in dom (Del (p,i)) holds
(Del (p,i)) . b₂ = (Del (q,i)) . b₂ ) )
p <> {} by A6;
then consider m being Nat such that
A8: len p = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A9: len (Del (p,i)) = m by A6, A8, FINSEQ_3:109;
hence len (Del (q,i)) = len (Del (p,i)) by A1, A2, A3, A5, A4, A6, A8, FINSEQ_1:6, FINSEQ_3:109; :: thesis: for j being Nat st j in dom (Del (p,i)) holds
(Del (p,i)) . b₂ = (Del (q,i)) . b₂
let j be Nat; :: thesis: ( j in dom (Del (p,i)) implies (Del (p,i)) . b₁ = (Del (q,i)) . b₁ )
assume j in dom (Del (p,i)) ; :: thesis: (Del (p,i)) . b₁ = (Del (q,i)) . b₁
then A10: j <= m by A7, A9, FINSEQ_1:1;

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

suppose A11: j < i ; :: thesis: (Del (p,i)) . b₁ = (Del (q,i)) . b₁

hence (Del (p,i)) . j = p . j by FINSEQ_3:110
.= (q +* (i,a)) . j by A1, A11, FUNCT_7:32
.= q . j by A11, FUNCT_7:32
.= (Del (q,i)) . j by A11, FINSEQ_3:110 ;
:: thesis: verum

end;

suppose A12: i <= j ; :: thesis: (Del (p,i)) . b₁ = (Del (q,i)) . b₁

then A13: j + 1 > i by NAT_1:13;
thus (Del (p,i)) . j = p . (j + 1) by A6, A8, A10, A12, FINSEQ_3:111
.= (q +* (i,a)) . (j + 1) by A1, A13, FUNCT_7:32
.= q . (j + 1) by A13, FUNCT_7:32
.= (Del (q,i)) . j by A1, A2, A3, A5, A4, A6, A8, A10, A12, FINSEQ_1:6, FINSEQ_3:111 ; :: thesis: verum

end;

end;

end;

hence Del (p,i) = Del (q,i) by FINSEQ_2:9; :: thesis: verum

end;

suppose A14: not i in dom p ; :: thesis: Del (p,i) = Del (q,i)

then p +* (i,a) = p by FUNCT_7:def 3;
hence Del (p,i) = Del (q,i) by A1, A3, A14, FUNCT_7:def 3; :: thesis: verum

end;

end;