for m being CR_Sequence
for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) holds
card the carrier of (product X) = Product m