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