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
SubFin (M,k) = SubFin ((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
SubFin (M,k) = SubFin ((SubFin (M,n)),k)
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S st k <= n & n <= m holds
SubFin (M,k) = SubFin ((SubFin (M,n)),k)
let M be sigmaMeasureFamily of S; :: thesis: ( k <= n & n <= m implies SubFin (M,k) = SubFin ((SubFin (M,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: SubFin (M,k) = SubFin ((SubFin (M,n)),k)
SubFin ((SubFin (M,n)),k) = (SubFin (M,n)) | k by A1, Def9;
then SubFin ((SubFin (M,n)),k) = (M | n) | k by A2, Def9;
then SubFin ((SubFin (M,n)),k) = M | k by A1, FINSEQ_1:82;
hence SubFin (M,k) = SubFin ((SubFin (M,n)),k) by Def9, A1, A2, XXREAL_0:2; :: thesis: verum