theorem Th11: :: MEASUR14:11

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