:: deftheorem Def16 defines Chains CHAIN_1:def 16 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for b₄ being strict AbGroup holds
( b₄ = Chains (k,G) iff ( the carrier of b₄ = bool (cells (k,G)) & 0. b₄ = 0_ (k,G) & ( for A, B being Element of b₄
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) ) );