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
A0: {} in Indep B,P

proof

B0: {} is Element of Sigma by PROB_1:52;
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;

hence {} in Indep B,P by B0, Def1; :: thesis: verum

end;

A1: 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 B0: ( rng g c= Indep B,P & g is disjoint_valued ) ; :: thesis: Union g in Indep B,P

now

let n be Element of 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:12;
hence g . n is Element of Sigma by B0, 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 4;
hence g . n is Element of Sigma by PROB_1:10; :: thesis: verum

end;

end;

end;

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

end;

then reconsider g = g as SetSequence of by PROB_1:57;
B1: 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:12;
hence g . n in Indep B,P by B0; :: thesis: verum

end;

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

hence g . n in Indep B,P by A0, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

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

end;

reconsider Ug = Union g as Element of Sigma by PROB_1:58;
for b being Element of B holds P . (Ug /\ b) = (P . Ug) * (P . b) by B0, B1, Th2;
hence Union g in Indep B,P by Def1; :: thesis: verum

end;

A2: 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 B0: Z in Indep B,P ; :: thesis: Z ` in Indep B,P
then reconsider Z = Z as Event of Sigma ;
B1: 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 B0, Def1;
then b,Z are_independent_respect_to P by PROB_2:def 5;
then b,([#] Sigma) \ Z are_independent_respect_to P by PROB_2:37;
hence P . ((Z ` ) /\ b) = (P . (Z ` )) * (P . b) by PROB_2:def 5; :: thesis: verum

end;

reconsider Z' = Z ` as Element of Sigma by PROB_1:50;
Z' in Indep B,P by B1, Def1;
hence Z ` in Indep B,P ; :: thesis: verum

end;

reconsider Indp = Indep B,P as Subset-Family of Omega by XBOOLE_1:1;
Indp is Dynkin_System of Omega by A0, A1, A2, DYNKIN:def 7;
hence Indep B,P is Dynkin_System of Omega ; :: thesis: verum