let Omega, I 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
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:51;
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 12;
A1 . n in S by A3, A5;
then (A1 . n) ` is Event of S by PROB_1:20;
then (A1 . n) ` in S ;
hence (Complement A1) . n in S by PROB_1:def 2; :: thesis: verum

end;

then rng (Complement A1) c= S by NAT_1:52;
then reconsider CA1 = Complement A1 as SetSequence of S by RELAT_1:def 19;
Union CA1 in S by PROB_1:17;
then (Union (Complement A1)) ` is Event of S by PROB_1:20;
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:20;
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:15; :: thesis: verum