theorem Th4: :: MATRIXJ1:4

for i, n being Nat
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