let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let P be Probability of Sigma; :: thesis: for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let B be non empty Subset of Sigma; :: thesis: Indep (B,P) is Dynkin_System of Omega
A1: for b being Element of B holds P . ({} /\ b) = (P . {}) * (P . b)

proof

let b be Element of B; :: thesis: P . ({} /\ b) = (P . {}) * (P . b)
reconsider b = b as Event of Sigma ;
P . ({} /\ b) = 0 by VALUED_0:def 19;
hence P . ({} /\ b) = (P . {}) * (P . b) ; :: thesis: verum

end;

reconsider Indp = Indep (B,P) as Subset-Family of Omega by XBOOLE_1:1;
{} is Element of Sigma by PROB_1:22;
then A2: {} in Indep (B,P) by A1, Def1;
A3: for g being SetSequence of Omega st rng g c= Indep (B,P) & g is disjoint_valued holds
Union g in Indep (B,P)

proof

let g be SetSequence of Omega; :: thesis: ( rng g c= Indep (B,P) & g is disjoint_valued implies Union g in Indep (B,P) )
assume that
A4: rng g c= Indep (B,P) and
A5: g is disjoint_valued ; :: thesis: Union g in Indep (B,P)

now :: thesis: for n being Nat holds g . n is Event of Sigma

let n be Nat; :: thesis: g . n is Event of Sigma
g . n is Element of Sigma

proof

per cases ( n in dom g or not n in dom g ) ;

suppose n in dom g ; :: thesis: g . n is Element of Sigma

then g . n in rng g by FUNCT_1:3;
hence g . n is Element of Sigma by A4, TARSKI:def 3; :: thesis: verum

end;

suppose not n in dom g ; :: thesis: g . n is Element of Sigma

then g . n = {} by FUNCT_1:def 2;
hence g . n is Element of Sigma by PROB_1:4; :: thesis: verum

end;

end;

end;

hence g . n is Event of Sigma ; :: thesis: verum

end;

then reconsider g = g as SetSequence of Sigma by PROB_1:25;
reconsider Ug = Union g as Element of Sigma by PROB_1:26;
for n being Element of NAT
for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)

proof

let n be Element of NAT ; :: thesis: for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
let b be Element of B; :: thesis: P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
g . n in Indep (B,P)

proof

per cases ( n in dom g or not n in dom g ) ;

suppose n in dom g ; :: thesis: g . n in Indep (B,P)

then g . n in rng g by FUNCT_1:3;
hence g . n in Indep (B,P) by A4; :: thesis: verum

end;

suppose not n in dom g ; :: thesis: g . n in Indep (B,P)

hence g . n in Indep (B,P) by A2, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence P . ((g . n) /\ b) = (P . (g . n)) * (P . b) by Def1; :: thesis: verum

end;

then for b being Element of B holds P . (Ug /\ b) = (P . Ug) * (P . b) by A5, Th4;
hence Union g in Indep (B,P) by Def1; :: thesis: verum

end;

for Z being Subset of Omega st Z in Indep (B,P) holds
Z ` in Indep (B,P)

proof

let Z be Subset of Omega; :: thesis: ( Z in Indep (B,P) implies Z ` in Indep (B,P) )
assume A6: Z in Indep (B,P) ; :: thesis: Z ` in Indep (B,P)
then reconsider Z = Z as Event of Sigma ;
reconsider Z9 = Z ` as Element of Sigma by PROB_1:20;
for b being Element of B holds P . ((Z `) /\ b) = (P . (Z `)) * (P . b)

proof

let b be Element of B; :: thesis: P . ((Z `) /\ b) = (P . (Z `)) * (P . b)
P . (b /\ Z) = (P . b) * (P . Z) by A6, Def1;
then b,Z are_independent_respect_to P by PROB_2:def 4;
then b,([#] Sigma) \ Z are_independent_respect_to P by PROB_2:25;
hence P . ((Z `) /\ b) = (P . (Z `)) * (P . b) by PROB_2:def 4; :: thesis: verum

end;

then Z9 in Indep (B,P) by Def1;
hence Z ` in Indep (B,P) ; :: thesis: verum

end;

then Indp is Dynkin_System of Omega by A2, A3, DYNKIN:def 5;
hence Indep (B,P) is Dynkin_System of Omega ; :: thesis: verum