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_{1}( set ) -> Element of ExtREAL = M . (F " $1);

A1: for y being set st y in S2 holds

H_{1}(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_{1}(y)
from FUNCT_2:sch 11(A1);

A3: for y being Element of S2 holds N . y = H_{1}(y)
by A2;

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

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

A1: for y being set st y in S2 holds

H

consider N being Function of S2,ExtREAL such that

A2: for y being set st y in S2 holds

N . y = H

A3: for y being Element of S2 holds N . y = H

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

then A4:
N is V91()
by MEASURE1:def 2;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;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

now :: thesis: for A, B being Element of S2 st A misses B holds

N . (A \/ B) = (N . A) + (N . B)

then A9:
N is additive
by MEASURE1:def 8;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;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

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