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

proof

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;

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

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 )

proof

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;

then (Omega --> the Element of Omega2) " x = Omega by TARSKI:2;
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;

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

proof

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;

then (Omega --> the Element of Omega2) " x = {} by XBOOLE_0:def 1;
hence (Omega --> the Element of Omega2) " x in F by PROB_1:4; :: thesis: verum

end;

end;

end;

hence for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds
f is F,F2 -random_variable-like ; :: thesis: verum