let X be set ; :: thesis:
let S be SigmaRing of X; :: thesis:

let F be SetSequence of X; :: thesis:
assume A1: rng F c= S ; :: thesis:
then A2: Union F in S by DefSigmaRing;
reconsider UF = Union F as Subset of X ;

let x be object ; :: thesis:
assume BB: x in Intersection F ; :: thesis:
B0: Intersection F c= UF by SETLIM_1:9;

assume x in Union (UF (\) F) ; :: thesis:
then consider m being Nat such that
B1: x in (UF (\) F) . m by PROB_1:12;
x in UF \ (F . m) by B1, SETLIM_2:def 7;
then not x in F . m by XBOOLE_0:def 5;
hence contradiction by BB, PROB_1:13; :: thesis:

end;

hence x in UF \ (Union (UF (\) F)) by BB, B0, XBOOLE_0:def 5; :: thesis:

end;

then B3: Intersection F c= UF \ (Union (UF (\) F)) ;

let x be object ; :: thesis:
assume x in UF \ (Union (UF (\) F)) ; :: thesis:
then C3: ( x in UF & not x in Union (UF (\) F) ) by XBOOLE_0:def 5;

hereby :: thesis:

assume not x in Intersection F ; :: thesis:
then consider n being Nat such that
C2: not x in F . n by PROB_1:13;
x in UF \ (F . n) by C3, C2, XBOOLE_0:def 5;
then x in (UF (\) F) . n by SETLIM_2:def 7;
hence contradiction by C3, PROB_1:12; :: thesis:

end;

end;

then UF \ (Union (UF (\) F)) c= Intersection F ;
then B5: Intersection F = (Union F) \ (Union (UF (\) F)) by B3;

let x be object ; :: thesis:
assume x in rng (UF (\) F) ; :: thesis:
then consider n being Element of NAT such that
D1: x = (UF (\) F) . n by FUNCT_2:113;
D2: x = UF \ (F . n) by D1, SETLIM_2:def 7;
F . n in rng F by FUNCT_2:112;
hence x in S by A1, D2, A2, FINSUB_1:def 3; :: thesis:

end;

then rng (UF (\) F) c= S ;
then Union (UF (\) F) in S by DefSigmaRing;
hence Intersection F in S by A2, B5, FINSUB_1:def 3; :: thesis:

end;

hence S is sigma-multiplicative by PROB_1:def 6; :: thesis: