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;
A0: 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 Z: 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 C0: S in futSigmaFields F,I ; :: thesis: A ` in S
then C1: A in S by Z, SETFAM_1:def 1;
consider E being finite Subset of I such that
C2: S = sigUn F,(I \ E) by C0, Def7;
A ` is Event of sigma (Union (F | (I \ E))) by PROB_1:50, C1, C2;
hence A ` in S by C2; :: thesis: verum

end;

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

end;

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 B0: rng A1 c= tailSigmaField F,I ; :: thesis: Intersection A1 in tailSigmaField F,I
B1: 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 )
assume C0: S in futSigmaFields F,I ; :: thesis: A1 . n in S
A1 . n in rng A1 by NAT_1:52;
hence A1 . n in S by C0, SETFAM_1:def 1, B0; :: 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 C0: S in futSigmaFields F,I ; :: thesis: (Union (Complement A1)) ` in S
then consider E being finite Subset of I such that
C1: S = sigUn F,(I \ E) by Def7;
reconsider S = S as SigmaField of Omega by C1;
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 C0, B1;
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 PROB_1:def 9;
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;

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