1 <= n by NAT_1:14;
then A2: n in Seg m by A1;
ElmFin (X,n) = X . n by Def1, A1;
hence S . n is SigmaField of (ElmFin (X,n)) by A2, Def2; :: thesis: verum