for m being FinSequence of NAT
for X being non-empty non empty FinSequence st len m = len X & ( for i being Element of NAT st i in dom X holds
card (X . i) = m . i ) holds
card (product X) = Product m