let X be set ; :: thesis: for S being SigmaField of X

for F being sequence of S holds rng F is N_Sub_set_fam of X

let S be SigmaField of X; :: thesis: for F being sequence of S holds rng F is N_Sub_set_fam of X

let F be sequence of S; :: thesis: rng F is N_Sub_set_fam of X

ex H being sequence of (bool X) st rng F = rng H

for F being sequence of S holds rng F is N_Sub_set_fam of X

let S be SigmaField of X; :: thesis: for F being sequence of S holds rng F is N_Sub_set_fam of X

let F be sequence of S; :: thesis: rng F is N_Sub_set_fam of X

ex H being sequence of (bool X) st rng F = rng H

proof

hence
rng F is N_Sub_set_fam of X
by SUPINF_2:def 8; :: thesis: verum
rng F c= bool X
;

then reconsider F = F as sequence of (bool X) by FUNCT_2:6;

take F ; :: thesis: rng F = rng F

thus rng F = rng F ; :: thesis: verum

end;then reconsider F = F as sequence of (bool X) by FUNCT_2:6;

take F ; :: thesis: rng F = rng F

thus rng F = rng F ; :: thesis: verum