theorem :: MEASUR13:16

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence
for P being SemialgebraFamily of ProdFinSeq X st n <= m holds
P . n is semialgebra_of_sets of CarProduct (SubFin (X,n))