let i, n be Nat; :: thesis: for D being non empty set
for d being Element of D st i in Seg (n + 1) holds
Del ((n + 1) |-> d),i = n |-> d
let D be non empty set ; :: thesis: for d being Element of D st i in Seg (n + 1) holds
Del ((n + 1) |-> d),i = n |-> d
let d be Element of D; :: thesis: ( i in Seg (n + 1) implies Del ((n + 1) |-> d),i = n |-> d )
assume A1: i in Seg (n + 1) ; :: thesis: Del ((n + 1) |-> d),i = n |-> d
set n1 = n + 1;
set n1d = (n + 1) |-> d;
set nd = n |-> d;
set Dn = Del ((n + 1) |-> d),i;
A2: ( len ((n + 1) |-> d) = n + 1 & len (n |-> d) = n & dom ((n + 1) |-> d) = Seg (len ((n + 1) |-> d)) ) by FINSEQ_1:def 3, FINSEQ_1:def 18;
then A3: len (Del ((n + 1) |-> d),i) = n by A1, FINSEQ_3:118;

now

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (n |-> d) . j = (Del ((n + 1) |-> d),i) . j )
assume A4: ( 1 <= j & j <= n ) ; :: thesis: (n |-> d) . j = (Del ((n + 1) |-> d),i) . j
A5: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
j <= n + 1 by A4, NAT_1:13;
then A6: ( j in Seg (n + 1) & j in Seg n ) by A4, FINSEQ_1:3;
then A7: j + 1 in Seg (n + 1) by FINSEQ_1:81;

now

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

suppose j < i ; :: thesis: (Del ((n + 1) |-> d),i) . j = (n |-> d) . j

hence (Del ((n + 1) |-> d),i) . j = ((n + 1) |-> d) . j by A2, A5, FINSEQ_3:119
.= d by A6, FINSEQ_2:71
.= (n |-> d) . j by A6, FINSEQ_2:71 ;
:: thesis: verum

end;

suppose j >= i ; :: thesis: (Del ((n + 1) |-> d),i) . j = (n |-> d) . j

hence (Del ((n + 1) |-> d),i) . j = ((n + 1) |-> d) . (j + 1) by A1, A2, A4, A5, FINSEQ_3:120
.= d by A7, FINSEQ_2:71
.= (n |-> d) . j by A6, FINSEQ_2:71 ;
:: thesis: verum

end;

end;

end;

hence (n |-> d) . j = (Del ((n + 1) |-> d),i) . j ; :: thesis: verum

end;

hence Del ((n + 1) |-> d),i = n |-> d by A2, A3, FINSEQ_1:18; :: thesis: verum