set X = set_of_random_variables_on (F,F2);
ex z being Function of Omega,Omega2 st z is F,F2 -random_variable-like
proof
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
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 ;
hence s in (Omega --> the Element of Omega2) " x by ; :: 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 ex z being Function of Omega,Omega2 st z is F,F2 -random_variable-like by A1; :: thesis: verum
end;
then consider z being Function of Omega,Omega2 such that
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