1 <= n by NAT_1:14;
then n in Seg m by A1;
then consider Si being SigmaField of (X . n) such that
A2: ( Si = S . n & M . n is sigma_Measure of Si ) by Def8;
A3: X . n = ElmFin (X,n) by Def1, A1;
Si = ElmFin (S,n) by Def7, A1, A2;
hence M . n is sigma_Measure of (ElmFin (S,n)) by A2, A3; :: thesis: verum