let Omega1, Omega2 be non empty set ; :: thesis: for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
let S1 be SigmaField of Omega1; :: thesis: for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
let S2 be SigmaField of Omega2; :: thesis: for M being Measure of S1
for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
let M be Measure of S1; :: thesis: for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
let F be random_variable of S1,S2; :: thesis: ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
deffunc H₁( set ) -> Element of ExtREAL = M . (F " $1);
A1: for y being set st y in S2 holds
H₁(y) in ExtREAL ;
consider N being Function of S2,ExtREAL such that
A2: for y being set st y in S2 holds
N . y = H₁(y) from FUNCT_2:sch 11(A1);
A3: for y being Element of S2 holds N . y = H₁(y) by A2;

now :: thesis: for A being Element of S2 holds 0. <= N . A

let A be Element of S2; :: thesis: 0. <= N . A
F " A in S1 by FINANCE1:def 5;
then 0. <= M . (F " A) by MEASURE1:def 2;
hence 0. <= N . A by A2; :: thesis: verum

end;

then A4: N is nonnegative by MEASURE1:def 2;

now :: thesis: for A, B being Element of S2 st A misses B holds
N . (A \/ B) = (N . A) + (N . B)

let A, B be Element of S2; :: thesis: ( A misses B implies N . (A \/ B) = (N . A) + (N . B) )
assume A5: A misses B ; :: thesis: N . (A \/ B) = (N . A) + (N . B)
A6: (F " A) /\ (F " B) = F " (A /\ B) by FUNCT_1:68
.= F " {} by A5
.= {} ;
A7: F " A in S1 by FINANCE1:def 5;
A8: F " B in S1 by FINANCE1:def 5;
thus N . (A \/ B) = M . (F " (A \/ B)) by A2
.= M . ((F " A) \/ (F " B)) by RELAT_1:140
.= (M . (F " A)) + (M . (F " B)) by A6, A7, A8, MEASURE1:def 8, XBOOLE_0:def 7
.= (N . A) + (M . (F " B)) by A2
.= (N . A) + (N . B) by A2 ; :: thesis: verum

end;

then A9: N is additive by MEASURE1:def 8;
N . {} = M . (F " {}) by A2, PROB_1:4
.= 0 by VALUED_0:def 19 ;
then N is zeroed by VALUED_0:def 19;
hence ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y) by A3, A4, A9; :: thesis: verum