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 DefPRD;
thus (Product-Probability Omega1,Omega2,P1,P2) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2) by LMXY10A, A1; :: thesis: verum