theorem Th12: :: MEASUR14:12

for m being non zero Nat
for X being non-empty b₁ -element FinSequence holds CarProd X is bijective