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
SubFin (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
SubFin (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
SubFin (M,n) is sigma_finite
let M be sigmaMeasureFamily of S; :: thesis: ( n <= m & M is sigma_finite implies SubFin (M,n) is sigma_finite )
assume that
A1: n <= m and
A2: M is sigma_finite ; :: thesis: SubFin (M,n) is sigma_finite
set Xn = SubFin (X,n);
set Sn = SubFin (S,n);
set Mn = SubFin (M,n);
A3: ( SubFin (X,n) = X | n & SubFin (S,n) = S | n & SubFin (M,n) = M | n ) by A1, Def5, Def6, Def9;
A4: Seg n c= Seg m by A1, FINSEQ_1:5;
for j being Nat st j in Seg n holds
ex Xj being non empty set ex Sj being SigmaField of Xj ex Mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite )

proof

let j be Nat; :: thesis: ( j in Seg n implies ex Xj being non empty set ex Sj being SigmaField of Xj ex Mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite ) )
assume A5: j in Seg n ; :: thesis: ex Xj being non empty set ex Sj being SigmaField of Xj ex Mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite )
then consider Xj being non empty set , Sj being SigmaField of Xj, Mj being sigma_Measure of Sj such that
A6: ( Xj = X . j & Sj = S . j & Mj = M . j & Mj is sigma_finite ) by A2, A4;
take Xj ; :: thesis: ex Sj being SigmaField of Xj ex Mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite )
take Sj ; :: thesis: ex Mj being sigma_Measure of Sj st
( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite )
take Mj ; :: thesis: ( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite )
thus ( Xj = (SubFin (X,n)) . j & Sj = (SubFin (S,n)) . j & Mj = (SubFin (M,n)) . j & Mj is sigma_finite ) by A3, A5, A6, FUNCT_1:49; :: thesis: verum

end;

hence SubFin (M,n) is sigma_finite ; :: thesis: verum