let Omega, Omega2 be non empty set ; :: thesis: for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

let F be SigmaField of Omega; :: thesis: for F2 being SigmaField of Omega2

for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

let F2 be SigmaField of Omega2; :: thesis: for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

set k = the Element of Omega2;

set z = Omega --> the Element of Omega2;

for x being Element of F2 holds (Omega --> the Element of Omega2) " x in F

f is F,F2 -random_variable-like ; :: thesis: verum

for F2 being SigmaField of Omega2

for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

let F be SigmaField of Omega; :: thesis: for F2 being SigmaField of Omega2

for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

let F2 be SigmaField of Omega2; :: thesis: for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

set k = the Element of Omega2;

set z = Omega --> the Element of Omega2;

for x being Element of F2 holds (Omega --> the Element of Omega2) " x in F

proof

hence
for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds
let x be Element of F2; :: thesis: (Omega --> the Element of Omega2) " x in F

set K = (Omega --> the Element of Omega2) " x;

A2: dom (Omega --> the Element of Omega2) = Omega by FUNCT_2:def 1;

end;set K = (Omega --> the Element of Omega2) " x;

A2: dom (Omega --> the Element of Omega2) = Omega by FUNCT_2:def 1;

per cases
( the Element of Omega2 in x or not the Element of Omega2 in x )
;

end;

suppose A3:
the Element of Omega2 in x
; :: thesis: (Omega --> the Element of Omega2) " x in F

for s being object holds

( s in (Omega --> the Element of Omega2) " x iff s in Omega )

then (Omega --> the Element of Omega2) " x is Element of F by PROB_1:23;

hence (Omega --> the Element of Omega2) " x in F ; :: thesis: verum

end;( s in (Omega --> the Element of Omega2) " x iff s in Omega )

proof

then
(Omega --> the Element of Omega2) " x = Omega
by TARSKI:2;
let s be object ; :: thesis: ( s in (Omega --> the Element of Omega2) " x iff s in Omega )

thus ( s in (Omega --> the Element of Omega2) " x implies s in Omega ) ; :: thesis: ( s in Omega implies s in (Omega --> the Element of Omega2) " x )

assume s in Omega ; :: thesis: s in (Omega --> the Element of Omega2) " x

then ( s in Omega & (Omega --> the Element of Omega2) . s in x ) by A3, FUNCOP_1:7;

hence s in (Omega --> the Element of Omega2) " x by A2, FUNCT_1:def 7; :: thesis: verum

end;thus ( s in (Omega --> the Element of Omega2) " x implies s in Omega ) ; :: thesis: ( s in Omega implies s in (Omega --> the Element of Omega2) " x )

assume s in Omega ; :: thesis: s in (Omega --> the Element of Omega2) " x

then ( s in Omega & (Omega --> the Element of Omega2) . s in x ) by A3, FUNCOP_1:7;

hence s in (Omega --> the Element of Omega2) " x by A2, FUNCT_1:def 7; :: thesis: verum

then (Omega --> the Element of Omega2) " x is Element of F by PROB_1:23;

hence (Omega --> the Element of Omega2) " x in F ; :: thesis: verum

suppose A4:
not the Element of Omega2 in x
; :: thesis: (Omega --> the Element of Omega2) " x in F

for r being object holds not r in (Omega --> the Element of Omega2) " x

hence (Omega --> the Element of Omega2) " x in F by PROB_1:4; :: thesis: verum

end;proof

then
(Omega --> the Element of Omega2) " x = {}
by XBOOLE_0:def 1;
let r be object ; :: thesis: not r in (Omega --> the Element of Omega2) " x

assume r in (Omega --> the Element of Omega2) " x ; :: thesis: contradiction

then ( r in dom (Omega --> the Element of Omega2) & (Omega --> the Element of Omega2) . r in x ) by FUNCT_1:def 7;

hence contradiction by A4, FUNCOP_1:7; :: thesis: verum

end;assume r in (Omega --> the Element of Omega2) " x ; :: thesis: contradiction

then ( r in dom (Omega --> the Element of Omega2) & (Omega --> the Element of Omega2) . r in x ) by FUNCT_1:def 7;

hence contradiction by A4, FUNCOP_1:7; :: thesis: verum

hence (Omega --> the Element of Omega2) " x in F by PROB_1:4; :: thesis: verum

f is F,F2 -random_variable-like ; :: thesis: verum