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

A5: now :: thesis: for j being Nat st 1 <= j & j <= n holds
(n |-> d) . j = (Del (((n + 1) |-> d),i)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (n |-> d) . j = (Del (((n + 1) |-> d),i)) . j )
assume that
A6: 1 <= j and
A7: j <= n ; :: thesis: (n |-> d) . j = (Del (((n + 1) |-> d),i)) . j
j <= n + 1 by A7, NAT_1:13;
then A8: j in Seg (n + 1) by A6;
A9: j in Seg n by A6, A7;
then A10: j + 1 in Seg (n + 1) by FINSEQ_1:60;

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

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 FINSEQ_3:110
.= d by A8, FINSEQ_2:57
.= (n |-> d) . j by A9, FINSEQ_2:57 ;
:: 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, A2, A7, FINSEQ_3:111
.= d by A10, FINSEQ_2:57
.= (n |-> d) . j by A9, FINSEQ_2:57 ;
:: 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:109;
hence Del (((n + 1) |-> d),i) = n |-> d by A3, A5; :: thesis: verum