theorem :: CHAIN_1:57

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of k,G holds C + (0_ (k,G)) = C ;