let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
(ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n)
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st n <= m holds
(ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n)
let S be sigmaFieldFamily of X; :: thesis: ( n <= m implies (ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n) )
assume A1: n <= m ; :: thesis: (ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n)
1 <= n by NAT_1:14;
then n in Seg m by A1;
hence (ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n) by Def2; :: thesis: verum