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 (image_measure (F,(P2M P))) . Omega2 = 1

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 (image_measure (F,(P2M P))) . Omega2 = 1

let S2 be SigmaField of Omega2; :: thesis: for P being Probability of S1

for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1

let P be Probability of S1; :: thesis: for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1

let F be random_variable of S1,S2; :: thesis: (image_measure (F,(P2M P))) . Omega2 = 1

A1: for y being set st y in S2 holds

(image_measure (F,(P2M P))) . y = (P2M P) . (F " y) by Def6;

thus (image_measure (F,(P2M P))) . Omega2 = (P2M P) . (F " Omega2) by PROB_1:5, A1

.= (P2M P) . Omega1 by FUNCT_2:40

.= 1 by PROB_1:def 8 ; :: thesis: verum

for S2 being SigmaField of Omega2

for P being Probability of S1

for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1

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 (image_measure (F,(P2M P))) . Omega2 = 1

let S2 be SigmaField of Omega2; :: thesis: for P being Probability of S1

for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1

let P be Probability of S1; :: thesis: for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1

let F be random_variable of S1,S2; :: thesis: (image_measure (F,(P2M P))) . Omega2 = 1

A1: for y being set st y in S2 holds

(image_measure (F,(P2M P))) . y = (P2M P) . (F " y) by Def6;

thus (image_measure (F,(P2M P))) . Omega2 = (P2M P) . (F " Omega2) by PROB_1:5, A1

.= (P2M P) . Omega1 by FUNCT_2:40

.= 1 by PROB_1:def 8 ; :: thesis: verum