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

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 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 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 Sigma by PROB_1:57;
reconsider Ug = Union g as Element of Sigma by PROB_1:58;
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 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 4; :: 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:50;
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 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;

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 7;
hence Indep B,P is Dynkin_System of Omega ; :: thesis: verum