let i be Element of NAT ; :: thesis: for x being set
for p being FinSequence holds Del (p +* i,x),i = Del p,i
let x be set ; :: thesis: for p being FinSequence holds Del (p +* i,x),i = Del p,i
let p be FinSequence; :: 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 ( 1 <= i & i <= len p ) by FINSEQ_3:27;
then consider j being Nat such that
A2: len p = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A3: len p = j + 1 by A2;
A4: dom (p +* i,x) = dom p by FUNCT_7:32;
then A5: len (p +* i,x) = len p by FINSEQ_3:31;
len (Del (p +* i,x),i) = j by A1, A2, A4, A5, FINSEQ_3:118;
then X: dom (Del (p +* i,x),i) = Seg j by FINSEQ_1:def 3;

now

thus len (Del (p +* i,x),i) = j by A1, A2, A4, A5, FINSEQ_3:118; :: 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, A2, FINSEQ_3:118; :: 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 A6: ( 1 <= a & a <= j ) by X, FINSEQ_1:3;
A7: a in NAT by ORDINAL1:def 13;

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 A3, A5, A7, FINSEQ_3:119
.= p . a by A8, FUNCT_7:34
.= (Del p,i) . a by A3, A7, A8, FINSEQ_3:119 ;
:: 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, A2, A4, A5, A6, A7, A9, FINSEQ_3:120
.= p . (a + 1) by A10, FUNCT_7:34
.= (Del p,i) . a by A1, A2, A6, A7, A9, FINSEQ_3:120 ; :: thesis: verum

end;

end;

end;

hence Del (p +* i,x),i = Del p,i by FINSEQ_2:10; :: 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;