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)

A ` in tailSigmaField (F,I)

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

for A being Subset of Omega st A in tailSigmaField (F,I) holds
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

(Union (Complement A1)) ` in S

end;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

for S being set st S in futSigmaFields (F,I) holds
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;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

(Union (Complement A1)) ` in S

proof

hence
Intersection A1 in tailSigmaField (F,I)
by SETFAM_1:def 1; :: thesis: verum
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

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;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

then
rng (Complement A1) c= S
by NAT_1:52;
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;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

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

A ` in tailSigmaField (F,I)

proof

hence
tailSigmaField (F,I) is SigmaField of Omega
by A1, PROB_1:15; :: thesis: verum
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

end;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

hence
A ` in tailSigmaField (F,I)
by SETFAM_1:def 1; :: thesis: verum
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;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