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

proof

not { f where f is Function of X,COMPLEX : f | X is bounded } is empty
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;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

proof

hence
{ f where f is Function of X,COMPLEX : f | X is bounded } is non empty Subset of (CAlgebra X)
by A1; :: thesis: verum
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;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