:: deftheorem defines CarProd MEASUR14:def 6 :
for m being non zero Nat
for X being non-empty b₁ -element FinSequence holds CarProd X = (Pt2FinSeq X) . m;