let x be set ; :: thesis: for p being FinSequence
for i being Nat holds Del ((p +* (i,x)),i) = Del (p,i)
let p be FinSequence; :: thesis: for i being Nat holds Del ((p +* (i,x)),i) = Del (p,i)
let i be Nat; :: thesis: Del ((p +* (i,x)),i) = Del (p,i)
set f = p;

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

suppose A1: i in dom p ; :: thesis: Del ((p +* (i,x)),i) = Del (p,i)

then A2: i <= len p by FINSEQ_3:25;
1 <= i by A1, FINSEQ_3:25;
then consider j being Nat such that
A3: len p = j + 1 by A2, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A4: dom (p +* (i,x)) = dom p by FUNCT_7:30;
then A5: len (p +* (i,x)) = len p by FINSEQ_3:29;
then len (Del ((p +* (i,x)),i)) = j by A1, A3, A4, FINSEQ_3:109;
then A6: dom (Del ((p +* (i,x)),i)) = Seg j by FINSEQ_1:def 3;

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

thus len (Del ((p +* (i,x)),i)) = j by A1, A3, A4, A5, FINSEQ_3:109; :: thesis: ( len (Del (p,i)) = j & ( for a being Nat st a in dom (Del ((p +* (i,x)),i)) holds
(Del ((p +* (i,x)),i)) . b₂ = (Del (p,i)) . b₂ ) )
thus len (Del (p,i)) = j by A1, A3, FINSEQ_3:109; :: thesis: for a being Nat st a in dom (Del ((p +* (i,x)),i)) holds
(Del ((p +* (i,x)),i)) . b₂ = (Del (p,i)) . b₂
let a be Nat; :: thesis: ( a in dom (Del ((p +* (i,x)),i)) implies (Del ((p +* (i,x)),i)) . b₁ = (Del (p,i)) . b₁ )
assume a in dom (Del ((p +* (i,x)),i)) ; :: thesis: (Del ((p +* (i,x)),i)) . b₁ = (Del (p,i)) . b₁
then A7: a <= j by A6, FINSEQ_1:1;

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

suppose A8: a < i ; :: thesis: (Del ((p +* (i,x)),i)) . b₁ = (Del (p,i)) . b₁

hence (Del ((p +* (i,x)),i)) . a = (p +* (i,x)) . a by FINSEQ_3:110
.= p . a by A8, FUNCT_7:32
.= (Del (p,i)) . a by A8, FINSEQ_3:110 ;
:: thesis: verum

end;

suppose A9: i <= a ; :: thesis: (Del ((p +* (i,x)),i)) . b₁ = (Del (p,i)) . b₁

then A10: i < a + 1 by NAT_1:13;
thus (Del ((p +* (i,x)),i)) . a = (p +* (i,x)) . (a + 1) by A1, A3, A4, A5, A7, A9, FINSEQ_3:111
.= p . (a + 1) by A10, FUNCT_7:32
.= (Del (p,i)) . a by A1, A3, A7, A9, FINSEQ_3:111 ; :: thesis: verum

end;

end;

end;

hence Del ((p +* (i,x)),i) = Del (p,i) by FINSEQ_2:9; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: Del ((p +* (i,x)),i) = Del (p,i)

hence Del ((p +* (i,x)),i) = Del (p,i) by FUNCT_7:def 3; :: thesis: verum

end;

end;