let Omega, I be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let P be Probability of Sigma; :: thesis:
let a be Element of Sigma; :: thesis:
let F be ManySortedSigmaField of I,Sigma; :: thesis:
assume A0: F is_independent_wrt P ; :: thesis:
assume A1: a in tailSigmaField F,I ; :: thesis:
set Ie = I \ ({} I);
A2: ( a in tailSigmaField F,I implies a in sigUn F,(I \ ({} I)) )

proof

assume Z: a in tailSigmaField F,I ; :: thesis:
sigUn F,(I \ ({} I)) in futSigmaFields F,I by Def7;
hence a in sigUn F,(I \ ({} I)) by Z, SETFAM_1:def 1; :: thesis:

end;

A3: 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:
let p, q be Event of Sigma; :: thesis:
assume B0: ( p in sigUn F,E & 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:
sigUn F,(I \ E) in futSigmaFields F,I by Def7;
hence q in sigUn F,(I \ E) by B0, SETFAM_1:def 1; :: thesis:

end;

then B1: q in sigUn F,(I \ E) ;

per cases ;

suppose C0: ( E <> {} & I \ E <> {} ) ; :: thesis:

then reconsider E = E as non empty Subset of I ;
reconsider IE = I \ E as non empty Subset of I by C0;
E misses IE by XBOOLE_1:79;
then P . (p /\ q) = (P . p) * (P . q) by A0, B0, B1, Th14;
hence p,q are_independent_respect_to P by PROB_2:def 5; :: thesis:

end;

suppose C1: ( not E <> {} or not I \ E <> {} ) ; :: thesis:

reconsider e = {} as Subset of I by XBOOLE_1:2;
Union (F | {} ) = {} by ZFMISC_1:2;
then D2: sigUn F,e = {{} ,Omega} by Th1;
D3: for u, v being Event of Sigma st u in {{} ,Omega} holds
u,v are_independent_respect_to P

proof

let u, v be Event of Sigma; :: thesis:
assume E0: u in {{} ,Omega} ; :: thesis:

per cases ;

suppose u = {} ; :: thesis:

hence u,v are_independent_respect_to P by PROB_2:31, PROB_2:35; :: thesis:

end;

suppose u <> {} ; :: thesis:

then u = [#] Sigma by E0, TARSKI:def 2;
hence u,v are_independent_respect_to P by PROB_2:31, PROB_2:36; :: thesis:

end;

p,q are_independent_respect_to P

proof

per cases ;

suppose E = {} ; :: thesis:

hence p,q are_independent_respect_to P by D2, D3, B0; :: thesis:

end;

suppose E <> {} ; :: thesis:

hence p,q are_independent_respect_to P by D2, D3, B1, C1, PROB_2:31; :: thesis:

end;

hence p,q are_independent_respect_to P ; :: thesis:

end;

A4: 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:
assume B0: ( p in finSigmaFields F,I & q in tailSigmaField F,I ) ; :: thesis:
then consider E being finite Subset of I such that
B1: p in sigUn F,E by Def10;
thus p,q are_independent_respect_to P by B0, B1, A3; :: thesis:

end;

reconsider T = tailSigmaField F,I as SigmaField of Omega by Th16;
a5: T c= sigma T by PROB_1:def 14;
A6: sigma (finSigmaFields F,I) = sigUn F,(I \ ({} I))

proof

thus sigma (finSigmaFields F,I) c= sigUn F,(I \ ({} I)) :: according to XBOOLE_0:def 10 :: thesis:

proof

finSigmaFields F,I c= sigma (Union (F | (I \ ({} I))))

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume X in finSigmaFields F,I ; :: thesis:
then consider E being finite Subset of I such that
E0: X in sigUn F,E by Def10;
F | E c= F | (I \ ({} I)) by RELAT_1:104;
then E2: union (rng (F | E)) c= union (rng (F | (I \ ({} I)))) by RELAT_1:25, ZFMISC_1:95;
Union (F | (I \ ({} I))) c= sigma (Union (F | (I \ ({} I)))) by PROB_1:def 14;
then Union (F | E) c= sigma (Union (F | (I \ ({} I)))) by E2, XBOOLE_1:1;
then sigma (Union (F | E)) c= sigma (Union (F | (I \ ({} I)))) by PROB_1:def 14;
hence X in sigma (Union (F | (I \ ({} I)))) by E0; :: thesis:

end;

hence sigma (finSigmaFields F,I) c= sigUn F,(I \ ({} I)) by PROB_1:def 14; :: thesis:

end;

Union (F | (I \ ({} I))) c= sigma (finSigmaFields F,I)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume E0: x in Union (F | (I \ ({} I))) ; :: thesis:
dom F c= I \ ({} I) ;
then x in union (rng F) by E0, RELAT_1:97;
then consider y being set such that
E1: ( x in y & y in rng F ) by TARSKI:def 4;
consider i being set such that
E2: ( i in dom F & y = F . i ) by E1, FUNCT_1:def 5;
defpred S₁[ set ] means ex i being set st
( i in I & $1 in F . i );
consider X being set such that
E3: for z being set holds
( z in X iff ( z in finSigmaFields F,I & S₁[z] ) ) from XBOOLE_0:sch 1();
E4: x in X

proof

x in finSigmaFields F,I

proof

D0: dom (F | {i}) = (dom F) /\ {i} by RELAT_1:90
.= {i} by E2, ZFMISC_1:52 ;
then rng (F | {i}) = {((F | {i}) . i)} by FUNCT_1:14;
then D1: union (rng (F | {i})) = (F | {i}) . i by ZFMISC_1:31;
i in dom (F | {i}) by D0, TARSKI:def 1;
then D2: Union (F | {i}) = F . i by D1, FUNCT_1:70;
i in I by E2;
then for z being set 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;
reconsider Fi = F . i as SigmaField of Omega by E2, Def2;
D3: sigma Fi c= Fi by PROB_1:def 14;
Fi c= sigma Fi by PROB_1:def 14;
then D4: sigUn F,E = F . i by D2, D3, XBOOLE_0:def 10;
reconsider x = x as Subset of Omega by E1, E2;
thus x in finSigmaFields F,I by D4, E2, E1, Def10; :: thesis:

end;

hence x in X by E3, E2, E1; :: thesis:

end;

for z being set st z in X holds
z in finSigmaFields F,I by E3;
then E5: X c= finSigmaFields F,I by TARSKI:def 3;
finSigmaFields F,I c= sigma (finSigmaFields F,I) by PROB_1:def 14;
hence x in sigma (finSigmaFields F,I) by E4, E5, TARSKI:def 3; :: thesis:

end;

hence sigUn F,(I \ ({} I)) c= sigma (finSigmaFields F,I) by PROB_1:def 14; :: thesis:

end;

A7: 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

let u, v be Event of Sigma; :: thesis:
assume Z: ( u in sigUn F,(I \ ({} I)) & v in tailSigmaField F,I ) ; :: thesis:
C0: not finSigmaFields F,I is empty

proof

consider E being finite Subset of I;
{} in sigUn F,E by PROB_1:42;
hence not finSigmaFields F,I is empty by Def10; :: thesis:

end;

c0: finSigmaFields F,I c= Sigma

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in finSigmaFields F,I ; :: thesis:
then consider E being finite Subset of I such that
D0: x in sigUn F,E by Def10;
Union (F | E) c= Sigma

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in Union (F | E) ; :: thesis:
then consider S being set such that
F0: ( y in S & S in rng (F | E) ) by TARSKI:def 4;
thus y in Sigma by F0; :: thesis:

end;

then sigma (Union (F | E)) c= Sigma by PROB_1:def 14;
hence x in Sigma by D0; :: thesis:

end;

B2: finSigmaFields F,I is intersection_stable

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:
assume D0: ( x in finSigmaFields F,I & y in finSigmaFields F,I ) ; :: thesis:
then consider E1 being finite Subset of I such that
D1: x in sigUn F,E1 by Def10;
consider E2 being finite Subset of I such that
D2: y in sigUn F,E2 by D0, Def10;
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:
let E1, E2 be finite Subset of I; :: thesis:
assume Z: z in sigUn F,E1 ; :: thesis:
reconsider E3 = E1 \/ E2 as finite Subset of I ;
F1: Union (F | E1) c= Union (F | E3)

proof

end;

end;

then ( x in sigUn F,(E1 \/ E2) & y in sigUn F,(E2 \/ E1) ) by D1, D2;
then x /\ y in sigUn F,(E1 \/ E2) by FINSUB_1:def 2;
hence x /\ y in finSigmaFields F,I by Def10; :: thesis:

end;

hence finSigmaFields F,I is intersection_stable by FINSUB_1:def 2; :: thesis:

end;

tailSigmaField F,I c= Sigma

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume d0: x in tailSigmaField F,I ; :: thesis:
set Ie = I \ ({} I);
sigUn F,(I \ ({} I)) in futSigmaFields F,I by Def7;
then D1: x in sigma (Union (F | (I \ ({} I)))) by d0, SETFAM_1:def 1;
Union (F | (I \ ({} I))) c= Sigma

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in Union (F | (I \ ({} I))) ; :: thesis:
then consider S being set such that
F0: ( y in S & S in rng (F | (I \ ({} I))) ) by TARSKI:def 4;
thus y in Sigma by F0; :: thesis:

end;

then sigma (Union (F | (I \ ({} I)))) c= Sigma by PROB_1:def 14;
hence x in Sigma by D1; :: thesis:

end;

hence u,v are_independent_respect_to P by Th8, c0, C0, A4, B2, Z, A6, a5; :: thesis:

end;

a,a are_independent_respect_to P by A1, A2, A7;
then P . (a /\ a) = (P . a) * (P . a) by PROB_2:def 5;
hence ( P . a = 0 or P . a = 1 ) by Th15; :: thesis: