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 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of 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 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of 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 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y1 be non empty finite Subset of Omega1; :: thesis: for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
let Y2 be non empty finite Subset of Omega2; :: thesis: (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
set P = Product-Probability (Omega1,Omega2,P1,P2);
consider Q being Function of [:Omega1,Omega2:],REAL such that
A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds (Product-Probability (Omega1,Omega2,P1,P2)) . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) by Def2;
thus (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2) by Lm7, A1; :: thesis: verum