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

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

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

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

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

for F being random_variable of S1,S2

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let P be Probability of S1; :: thesis: for F being random_variable of S1,S2

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let F be random_variable of S1,S2; :: thesis: for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let y be set ; :: thesis: ( y in S2 implies (probability (F,P)) . y = P . (F " y) )

assume A1: y in S2 ; :: thesis: (probability (F,P)) . y = P . (F " y)

thus (probability (F,P)) . y = (image_measure (F,(P2M P))) . y by Th13

.= P . (F " y) by A1, Def6 ; :: thesis: verum

for S2 being SigmaField of Omega2

for P being Probability of S1

for F being random_variable of S1,S2

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

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

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

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

for F being random_variable of S1,S2

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let P be Probability of S1; :: thesis: for F being random_variable of S1,S2

for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let F be random_variable of S1,S2; :: thesis: for y being set st y in S2 holds

(probability (F,P)) . y = P . (F " y)

let y be set ; :: thesis: ( y in S2 implies (probability (F,P)) . y = P . (F " y) )

assume A1: y in S2 ; :: thesis: (probability (F,P)) . y = P . (F " y)

thus (probability (F,P)) . y = (image_measure (F,(P2M P))) . y by Th13

.= P . (F " y) by A1, Def6 ; :: thesis: verum