let X be set ; :: thesis: for Si being SigmaField of X
for ASeq being SetSequence of Si holds Union ASeq in Si

let Si be SigmaField of X; :: thesis: for ASeq being SetSequence of Si holds Union ASeq in Si
let ASeq be SetSequence of Si; :: thesis: Union ASeq in Si
A1: for A1 being SetSequence of X st rng A1 c= Si holds
for n being Nat holds () . n in Si
proof
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies for n being Nat holds () . n in Si )
assume A2: rng A1 c= Si ; :: thesis: for n being Nat holds () . n in Si
let n be Nat; :: thesis: () . n in Si
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & (A1 . n) ` in Si ) by ;
hence (Complement A1) . n in Si by Def2; :: thesis: verum
end;
A3: for A1 being SetSequence of X st rng A1 c= Si holds
Union (Complement ()) in Si
proof
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies Union (Complement ()) in Si )
assume rng A1 c= Si ; :: thesis: Union (Complement ()) in Si
then for n being Nat holds () . n in Si by A1;
then rng () c= Si by NAT_1:52;
then Intersection () in Si by Def6;
then ((Union (Complement ())) `) ` in Si by Def1;
hence Union (Complement ()) in Si ; :: thesis: verum
end;
A4: for A1 being SetSequence of X st rng A1 c= Si holds
Union A1 in Si
proof
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies Union A1 in Si )
assume rng A1 c= Si ; :: thesis: Union A1 in Si
then Union (Complement ()) in Si by A3;
hence Union A1 in Si ; :: thesis: verum
end;
rng ASeq c= Si by RELAT_1:def 19;
hence Union ASeq in Si by A4; :: thesis: verum