let Omega1, Omega2 be non empty set ; :: thesis: for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = image_measure (F,(P2M P))
let S1 be SigmaField of Omega1; :: thesis: for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = image_measure (F,(P2M P))
let S2 be SigmaField of Omega2; :: thesis: for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = image_measure (F,(P2M P))
let P be Probability of S1; :: thesis: for F being random_variable of S1,S2 holds probability (F,P) = image_measure (F,(P2M P))
let F be random_variable of S1,S2; :: thesis: probability (F,P) = image_measure (F,(P2M P))
(image_measure (F,(P2M P))) . Omega2 = 1 by Th12;
hence probability (F,P) = image_measure (F,(P2M P)) by PROB_4:def 2; :: thesis: verum