A1: not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty

proof

set g = the Real-Valued-Random-Variable of Sigma;
the Real-Valued-Random-Variable of Sigma in { f where f is Real-Valued-Random-Variable of Sigma : verum } ;
hence not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty ; :: thesis: verum

end;

{ f where f is Real-Valued-Random-Variable of Sigma : verum } c= Funcs (Omega,REAL)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Real-Valued-Random-Variable of Sigma : verum } or x in Funcs (Omega,REAL) )
assume x in { f where f is Real-Valued-Random-Variable of Sigma : verum } ; :: thesis: x in Funcs (Omega,REAL)
then consider f being Real-Valued-Random-Variable of Sigma such that
A2: x = f ;
thus x in Funcs (Omega,REAL) by A2, FUNCT_2:8; :: thesis: verum

end;

hence { f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega) by A1; :: thesis: verum