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

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