let X be set ; :: thesis: for S being SigmaField of X
for F being Function of NAT,S holds union (rng F) is Element of S
let S be SigmaField of X; :: thesis: for F being Function of NAT,S holds union (rng F) is Element of S
let F be Function of NAT,S; :: thesis: union (rng F) is Element of S
( rng F is N_Sub_set_fam of X & rng F c= S ) by Th52, RELAT_1:def 19;
hence union (rng F) is Element of S by Def9; :: thesis: verum