let X be set ; :: thesis: for S being SigmaField of X
for T being N_Measure_fam of S ex F being sequence of S st T = rng F
let S be SigmaField of X; :: thesis: for T being N_Measure_fam of S ex F being sequence of S st T = rng F
let T be N_Measure_fam of S; :: thesis: ex F being sequence of S st T = rng F
consider F being sequence of (bool X) such that
A1: T = rng F by SUPINF_2:def 8;
rng F c= S by A1, Def1;
then F is sequence of S by FUNCT_2:6;
then consider F being sequence of S such that
A2: T = rng F by A1;
take F ; :: thesis: T = rng F
thus T = rng F by A2; :: thesis: verum