theorem Th56: :: CHAIN_1:59

for k being Nat
for d being non zero Nat
for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,G)