let Omega1, Omega2 be non empty finite set ; 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; 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; 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 ; ( 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 )
; (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; verum