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 )
set n1 = n + 1;
set n1d = (n + 1) |-> d;
set nd = n |-> d;
set Dn = Del ((n + 1) |-> d),i;
A1: len ((n + 1) |-> d) = n + 1 by FINSEQ_1:def 18;
A2: dom ((n + 1) |-> d) = Seg (len ((n + 1) |-> d)) by FINSEQ_1:def 3;
A3: len (n |-> d) = n by FINSEQ_1:def 18;
assume A4: i in Seg (n + 1) ; :: thesis: Del ((n + 1) |-> d),i = n |-> d

A5: now

A6: i in NAT by ORDINAL1:def 13;
let j be Nat; :: thesis: ( 1 <= j & j <= n implies (n |-> d) . j = (Del ((n + 1) |-> d),i) . j )
assume that
A7: 1 <= j and
A8: j <= n ; :: thesis: (n |-> d) . j = (Del ((n + 1) |-> d),i) . j
j <= n + 1 by A8, NAT_1:13;
then A9: j in Seg (n + 1) by A7, FINSEQ_1:3;
A10: j in NAT by ORDINAL1:def 13;
A11: j in Seg n by A7, A8, FINSEQ_1:3;
then A12: 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 A1, A3, A6, A10, FINSEQ_3:119
.= d by A9, FINSEQ_2:71
.= (n |-> d) . j by A11, 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 A4, A1, A3, A2, A8, A10, FINSEQ_3:120
.= d by A12, FINSEQ_2:71
.= (n |-> d) . j by A11, FINSEQ_2:71 ;
:: thesis: verum

end;

end;

end;

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

end;

len (Del ((n + 1) |-> d),i) = n by A4, A1, A2, FINSEQ_3:118;
hence Del ((n + 1) |-> d),i = n |-> d by A3, A5, FINSEQ_1:18; :: thesis: verum