let i be Element of 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 dx = Del p,i;
set dy = Del q,i;
set xi = p +* i,a;
set yi = q +* i,a;
A2: ( dom (p +* i,a) = dom p & dom (q +* i,a) = dom q ) by FUNCT_7:32;
A3: ( Seg (len (p +* i,a)) = dom (p +* i,a) & Seg (len p) = dom p & Seg (len (q +* i,a)) = dom (q +* i,a) & Seg (len q) = dom q ) by FINSEQ_1:def 3;

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

suppose A4: i in dom p ; :: thesis: Del p,i = Del q,i

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

now

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 A4;
then len p <> 0 ;
then consider m being Nat such that
A5: len p = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A6: len p = m + 1 by A5;
A7: len (Del p,i) = m by A4, A5, FINSEQ_3:118;
hence len (Del q,i) = len (Del p,i) by A1, A2, A3, A4, A5, FINSEQ_1:8, FINSEQ_3:118; :: 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 A8: j in dom (Del p,i) ; :: thesis: (Del p,i) . b₁ = (Del q,i) . b₁
A9: ( 1 <= j & j <= m ) by A7, A8, X, FINSEQ_1:3;
A10: j in NAT by ORDINAL1:def 13;

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 A6, A10, FINSEQ_3:119
.= (q +* i,a) . j by A1, A11, FUNCT_7:34
.= q . j by A11, FUNCT_7:34
.= (Del q,i) . j by A1, A2, A3, A6, A10, A11, FINSEQ_1:8, FINSEQ_3:119 ;
:: 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 A4, A5, A9, A10, A12, FINSEQ_3:120
.= (q +* i,a) . (j + 1) by A1, A13, FUNCT_7:34
.= q . (j + 1) by A13, FUNCT_7:34
.= (Del q,i) . j by A1, A2, A3, A4, A5, A9, A10, A12, FINSEQ_1:8, FINSEQ_3:120 ; :: thesis: verum

end;

end;

end;

hence Del p,i = Del q,i by FINSEQ_2:10; :: thesis: verum

end;

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

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

end;

end;