let I, Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField F,I is SigmaField of Omega
let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma holds tailSigmaField F,I is SigmaField of Omega
let F be ManySortedSigmaField of I,Sigma; :: thesis: tailSigmaField F,I is SigmaField of Omega
set T = tailSigmaField F,I;
A1: for A1 being SetSequence of Omega st rng A1 c= tailSigmaField F,I holds
Intersection A1 in tailSigmaField F,I

proof

let A1 be SetSequence of Omega; :: thesis: ( rng A1 c= tailSigmaField F,I implies Intersection A1 in tailSigmaField F,I )
assume A2: rng A1 c= tailSigmaField F,I ; :: thesis: Intersection A1 in tailSigmaField F,I
A3: for n being Element of NAT
for S being set st S in futSigmaFields F,I holds
A1 . n in S

proof

let n be Element of NAT ; :: thesis: for S being set st S in futSigmaFields F,I holds
A1 . n in S
let S be set ; :: thesis: ( S in futSigmaFields F,I implies A1 . n in S )
A4: A1 . n in rng A1 by NAT_1:52;
assume S in futSigmaFields F,I ; :: thesis: A1 . n in S
hence A1 . n in S by A2, A4, SETFAM_1:def 1; :: thesis: verum

end;

for S being set st S in futSigmaFields F,I holds
(Union (Complement A1)) ` in S

proof

let S be set ; :: thesis: ( S in futSigmaFields F,I implies (Union (Complement A1)) ` in S )
assume A5: S in futSigmaFields F,I ; :: thesis: (Union (Complement A1)) ` in S
then ex E being finite Subset of I st S = sigUn F,(I \ E) by Def7;
then reconsider S = S as SigmaField of Omega ;
for n being Nat holds (Complement A1) . n in S

proof

let n be Nat; :: thesis: (Complement A1) . n in S
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A1 . n in S by A3, A5;
then (A1 . n) ` is Event of S by PROB_1:50;
then (A1 . n) ` in S ;
hence (Complement A1) . n in S by PROB_1:def 4; :: thesis: verum

end;

then rng (Complement A1) c= S by NAT_1:53;
then reconsider CA1 = Complement A1 as SetSequence of S by RELAT_1:def 19;
Union CA1 in S by PROB_1:46;
then (Union (Complement A1)) ` is Event of S by PROB_1:50;
hence (Union (Complement A1)) ` in S ; :: thesis: verum

end;

hence Intersection A1 in tailSigmaField F,I by SETFAM_1:def 1; :: thesis: verum

end;

for A being Subset of Omega st A in tailSigmaField F,I holds
A ` in tailSigmaField F,I

proof

let A be Subset of Omega; :: thesis: ( A in tailSigmaField F,I implies A ` in tailSigmaField F,I )
assume A6: A in tailSigmaField F,I ; :: thesis: A ` in tailSigmaField F,I
for S being set st S in futSigmaFields F,I holds
A ` in S

proof

let S be set ; :: thesis: ( S in futSigmaFields F,I implies A ` in S )
assume A7: S in futSigmaFields F,I ; :: thesis: A ` in S
then consider E being finite Subset of I such that
A8: S = sigUn F,(I \ E) by Def7;
A in S by A6, A7, SETFAM_1:def 1;
then A ` is Event of sigma (Union (F | (I \ E))) by A8, PROB_1:50;
hence A ` in S by A8; :: thesis: verum

end;

hence A ` in tailSigmaField F,I by SETFAM_1:def 1; :: thesis: verum

end;

hence tailSigmaField F,I is SigmaField of Omega by A1, PROB_1:32; :: thesis: verum