let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for P being SemialgebraFamily of ProdFinSeq X st n <= m holds
P . n is semialgebra_of_sets of CarProduct (SubFin (X,n))
let X be non-empty m -element FinSequence; :: thesis: for P being SemialgebraFamily of ProdFinSeq X st n <= m holds
P . n is semialgebra_of_sets of CarProduct (SubFin (X,n))
let P be SemialgebraFamily of ProdFinSeq X; :: thesis: ( n <= m implies P . n is semialgebra_of_sets of CarProduct (SubFin (X,n)) )
assume A1: n <= m ; :: thesis: P . n is semialgebra_of_sets of CarProduct (SubFin (X,n))
1 <= n by NAT_1:14;
then n in Seg m by A1;
then P . n is semialgebra_of_sets of (ProdFinSeq X) . n by MEASUR10:def 2;
hence P . n is semialgebra_of_sets of CarProduct (SubFin (X,n)) by A1, Th4; :: thesis: verum