theorem :: MEASUR13:15

for m being non zero Nat
for X being non-empty b₁ -element FinSequence ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )