let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1

let P be Probability of Sigma; :: thesis: for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1

let a be Element of Sigma; :: thesis: for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1

let F be ManySortedSigmaField of I,Sigma; :: thesis: ( F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 implies P . a = 1 )
reconsider T = tailSigmaField (F,I) as SigmaField of Omega by Th15;
set Ie = I \ ({} I);
A1: ( a in tailSigmaField (F,I) implies a in sigUn (F,(I \ ({} I))) )
proof
assume A2: a in tailSigmaField (F,I) ; :: thesis: a in sigUn (F,(I \ ({} I)))
sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
hence a in sigUn (F,(I \ ({} I))) by ; :: thesis: verum
end;
assume A3: F is_independent_wrt P ; :: thesis: ( not a in tailSigmaField (F,I) or P . a = 0 or P . a = 1 )
A4: for E being finite Subset of I
for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P
proof
let E be finite Subset of I; :: thesis: for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P

let p, q be Event of Sigma; :: thesis: ( p in sigUn (F,E) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )
assume that
A5: p in sigUn (F,E) and
A6: q in tailSigmaField (F,I) ; :: thesis:
for E being finite Subset of I holds q in sigUn (F,(I \ E))
proof
let E be finite Subset of I; :: thesis: q in sigUn (F,(I \ E))
sigUn (F,(I \ E)) in futSigmaFields (F,I) by Def7;
hence q in sigUn (F,(I \ E)) by ; :: thesis: verum
end;
then A7: q in sigUn (F,(I \ E)) ;
per cases ( ( E <> {} & I \ E <> {} ) or not E <> {} or not I \ E <> {} ) ;
end;
end;
A13: for p, q being Event of Sigma st p in finSigmaFields (F,I) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P
proof
let p, q be Event of Sigma; :: thesis: ( p in finSigmaFields (F,I) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )
assume that
A14: p in finSigmaFields (F,I) and
A15: q in tailSigmaField (F,I) ; :: thesis:
ex E being finite Subset of I st p in sigUn (F,E) by ;
hence p,q are_independent_respect_to P by ; :: thesis: verum
end;
Union (F | (I \ ({} I))) c= sigma (finSigmaFields (F,I))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (F | (I \ ({} I))) or x in sigma (finSigmaFields (F,I)) )
assume x in Union (F | (I \ ({} I))) ; :: thesis: x in sigma (finSigmaFields (F,I))
then x in union (rng F) ;
then consider y being set such that
A16: x in y and
A17: y in rng F by TARSKI:def 4;
consider i being object such that
A18: i in dom F and
A19: y = F . i by ;
A20: x in finSigmaFields (F,I)
proof
reconsider Fi = F . i as SigmaField of Omega by ;
A21: ( sigma Fi c= Fi & Fi c= sigma Fi ) by PROB_1:def 9;
i in I by A18;
then for z being object st z in {i} holds
z in I by TARSKI:def 1;
then reconsider E = {i} as finite Subset of I by TARSKI:def 3;
A22: dom (F | {i}) = (dom F) /\ {i} by RELAT_1:61
.= {i} by ;
then rng (F | {i}) = {((F | {i}) . i)} by FUNCT_1:4;
then A23: union (rng (F | {i})) = (F | {i}) . i by ZFMISC_1:25;
i in dom (F | {i}) by ;
then Union (F | {i}) = F . i by ;
then sigUn (F,E) = F . i by A21;
hence x in finSigmaFields (F,I) by ; :: thesis: verum
end;
finSigmaFields (F,I) c= sigma (finSigmaFields (F,I)) by PROB_1:def 9;
hence x in sigma (finSigmaFields (F,I)) by A20; :: thesis: verum
end;
then A24: ( T c= sigma T & sigUn (F,(I \ ({} I))) c= sigma (finSigmaFields (F,I)) ) by PROB_1:def 9;
A25: for u, v being Event of Sigma st u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) holds
u,v are_independent_respect_to P
proof
for x, y being set st x in finSigmaFields (F,I) & y in finSigmaFields (F,I) holds
x /\ y in finSigmaFields (F,I)
proof
let x, y be set ; :: thesis: ( x in finSigmaFields (F,I) & y in finSigmaFields (F,I) implies x /\ y in finSigmaFields (F,I) )
assume that
A26: x in finSigmaFields (F,I) and
A27: y in finSigmaFields (F,I) ; :: thesis: x /\ y in finSigmaFields (F,I)
consider E1 being finite Subset of I such that
A28: x in sigUn (F,E1) by ;
consider E2 being finite Subset of I such that
A29: y in sigUn (F,E2) by ;
A30: for z being set
for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds
z in sigUn (F,(E1 \/ E2))
proof
let z be set ; :: thesis: for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds
z in sigUn (F,(E1 \/ E2))

let E1, E2 be finite Subset of I; :: thesis: ( z in sigUn (F,E1) implies z in sigUn (F,(E1 \/ E2)) )
reconsider E3 = E1 \/ E2 as finite Subset of I ;
A31: Union (F | E1) c= Union (F | E3)
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in Union (F | E1) or X in Union (F | E3) )
assume X in Union (F | E1) ; :: thesis: X in Union (F | E3)
then consider S being set such that
A32: X in S and
A33: S in rng (F | E1) by TARSKI:def 4;
F | E3 = (F | E1) \/ (F | E2) by RELAT_1:78;
then rng (F | E3) = (rng (F | E1)) \/ (rng (F | E2)) by RELAT_1:12;
then S in rng (F | E3) by ;
hence X in Union (F | E3) by ; :: thesis: verum
end;
Union (F | E3) c= sigma (Union (F | E3)) by PROB_1:def 9;
then Union (F | E1) c= sigma (Union (F | E3)) by A31;
then A34: sigma (Union (F | E1)) c= sigma (Union (F | E3)) by PROB_1:def 9;
assume z in sigUn (F,E1) ; :: thesis: z in sigUn (F,(E1 \/ E2))
hence z in sigUn (F,(E1 \/ E2)) by A34; :: thesis: verum
end;
then A35: y in sigUn (F,(E2 \/ E1)) by A29;
x in sigUn (F,(E1 \/ E2)) by ;
then x /\ y in sigUn (F,(E1 \/ E2)) by ;
hence x /\ y in finSigmaFields (F,I) by Def10; :: thesis: verum
end;
then A36: finSigmaFields (F,I) is intersection_stable by FINSUB_1:def 2;
let u, v be Event of Sigma; :: thesis: ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) implies u,v are_independent_respect_to P )
A37: not finSigmaFields (F,I) is empty
proof
set E = the finite Subset of I;
{} in sigUn (F, the finite Subset of I) by PROB_1:4;
hence not finSigmaFields (F,I) is empty by Def10; :: thesis: verum
end;
A38: tailSigmaField (F,I) c= Sigma
proof
set Ie = I \ ({} I);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tailSigmaField (F,I) or x in Sigma )
assume A39: x in tailSigmaField (F,I) ; :: thesis: x in Sigma
Union (F | (I \ ({} I))) c= Sigma
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union (F | (I \ ({} I))) or y in Sigma )
assume y in Union (F | (I \ ({} I))) ; :: thesis: y in Sigma
then ex S being set st
( y in S & S in rng (F | (I \ ({} I))) ) by TARSKI:def 4;
hence y in Sigma ; :: thesis: verum
end;
then A40: sigma (Union (F | (I \ ({} I)))) c= Sigma by PROB_1:def 9;
sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
then x in sigma (Union (F | (I \ ({} I)))) by ;
hence x in Sigma by A40; :: thesis: verum
end;
A41: finSigmaFields (F,I) c= Sigma
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in finSigmaFields (F,I) or x in Sigma )
assume x in finSigmaFields (F,I) ; :: thesis: x in Sigma
then consider E being finite Subset of I such that
A42: x in sigUn (F,E) by Def10;
Union (F | E) c= Sigma
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union (F | E) or y in Sigma )
assume y in Union (F | E) ; :: thesis: y in Sigma
then ex S being set st
( y in S & S in rng (F | E) ) by TARSKI:def 4;
hence y in Sigma ; :: thesis: verum
end;
then sigma (Union (F | E)) c= Sigma by PROB_1:def 9;
hence x in Sigma by A42; :: thesis: verum
end;
assume ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) ) ; :: thesis:
hence u,v are_independent_respect_to P by A13, A24, A37, A41, A36, A38, Th10; :: thesis: verum
end;
assume a in tailSigmaField (F,I) ; :: thesis: ( P . a = 0 or P . a = 1 )
then a,a are_independent_respect_to P by ;
then P . (a /\ a) = (P . a) * (P . a) by PROB_2:def 4;
hence ( P . a = 0 or P . a = 1 ) by Th2; :: thesis: verum