set X = set_of_random_variables_on (F,F2);

ex z being Function of Omega,Omega2 st z is F,F2 -random_variable-like

A5: z is F,F2 -random_variable-like ;

z in set_of_random_variables_on (F,F2) by A5;

hence not set_of_random_variables_on (F,F2) is empty ; :: thesis: verum

ex z being Function of Omega,Omega2 st z is F,F2 -random_variable-like

proof

then consider z being Function of Omega,Omega2 such that
set k = the Element of Omega2;

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

A1: ( Omega --> the Element of Omega2 is F,F2 -random_variable-like iff for x being set st x in F2 holds

(Omega --> the Element of Omega2) " x in F ) ;

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

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

A1: ( Omega --> the Element of Omega2 is F,F2 -random_variable-like iff for x being set st x in F2 holds

(Omega --> the Element of Omega2) " x in F ) ;

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

proof

hence
ex z being Function of Omega,Omega2 st z is F,F2 -random_variable-like
by A1; :: thesis: verum
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

A5: z is F,F2 -random_variable-like ;

z in set_of_random_variables_on (F,F2) by A5;

hence not set_of_random_variables_on (F,F2) is empty ; :: thesis: verum