let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m & M is sigma_finite holds
ElmFin (M,n) is sigma_finite
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m & M is sigma_finite holds
ElmFin (M,n) is sigma_finite
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S st n <= m & M is sigma_finite holds
ElmFin (M,n) is sigma_finite
let M be sigmaMeasureFamily of S; :: thesis: ( n <= m & M is sigma_finite implies ElmFin (M,n) is sigma_finite )
assume that
A1: n <= m and
A2: M is sigma_finite ; :: thesis: ElmFin (M,n) is sigma_finite
A3: Seg n c= Seg m by A1, FINSEQ_1:5;
A4: n in Seg n by FINSEQ_1:3;
A5: ( ElmFin (X,n) = X . n & ElmFin (S,n) = S . n & ElmFin (M,n) = M . n ) by A1, Def1, Def7, Def10;
ex Xi being non empty set ex Fi being SigmaField of Xi ex Mi being sigma_Measure of Fi st
( Xi = X . n & Fi = S . n & Mi = M . n & Mi is sigma_finite ) by A2, A3, A4;
hence ElmFin (M,n) is sigma_finite by A5; :: thesis: verum