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