A1: not { f where f is Function of X,REAL : f | X is bounded } is empty

proof

reconsider g = X --> (In (0,REAL)) as Function of X,REAL ;
g | X is bounded ;
then g in { f where f is Function of X,REAL : f | X is bounded } ;
hence not { f where f is Function of X,REAL : f | X is bounded } is empty ; :: thesis: verum

end;

{ f where f is Function of X,REAL : f | X is bounded } c= Funcs (X,REAL)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of X,REAL : f | X is bounded } or x in Funcs (X,REAL) )
assume x in { f where f is Function of X,REAL : f | X is bounded } ; :: thesis: x in Funcs (X,REAL)
then ex f being Function of X,REAL st
( x = f & f | X is bounded ) ;
hence x in Funcs (X,REAL) by FUNCT_2:8; :: thesis: verum

end;

hence { f where f is Function of X,REAL : f | X is bounded } is non empty Subset of (RAlgebra X) by A1; :: thesis: verum