let Omega1, Omega2 be non empty finite set ; :: thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let P1 be Probability of Trivial-SigmaField Omega1; :: thesis: for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
let y1, y2 be set ; :: thesis: ( y1 in Omega1 & y2 in Omega2 implies (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2}) )
assume A1: ( y1 in Omega1 & y2 in Omega2 ) ; :: thesis: (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
then A2: {y1} is finite Subset of Omega1 by ZFMISC_1:31;
for yy being object st yy in {y2} holds
yy in Omega2 by A1, TARSKI:def 1;
then A3: {y2} is finite Subset of Omega2 by TARSKI:def 3;
[:{y1},{y2}:] = {[y1,y2]} by ZFMISC_1:29;
hence (Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2}) by Th16, A2, A3; :: thesis: verum