theorem Th7: :: MEASUR14:7

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence st n <= m holds
(Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n)))