let m, n, k 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 k <= n & n <= m holds
ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st k <= n & n <= m holds
ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S st k <= n & n <= m holds
ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)
let M be sigmaMeasureFamily of S; :: thesis: ( k <= n & n <= m implies ElmFin (M,k) = ElmFin ((SubFin (M,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)
A3: ElmFin (M,k) = M . k by A1, A2, Def10, XXREAL_0:2;
1 <= k by NAT_1:14;
then A4: k in Seg n by A1;
SubFin (M,n) = M | n by A2, Def9;
then ElmFin ((SubFin (M,n)),k) = (M | n) . k by A1, Def10;
hence ElmFin (M,k) = ElmFin ((SubFin (M,n)),k) by A3, A4, FUNCT_1:49; :: thesis: verum