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

proof

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

end;

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

proof

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

end;

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