theorem Th58: :: CHAIN_1:61

for k being Nat
for d being non zero Nat
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)