set A = { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;
{ f where f is continuous Function of the carrier of X,COMPLEX : verum } c= Funcs ( the carrier of X,COMPLEX)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } or x in Funcs ( the carrier of X,COMPLEX) )
assume x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; :: thesis: x in Funcs ( the carrier of X,COMPLEX)
then ex f being continuous Function of the carrier of X,COMPLEX st x = f ;
hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; :: thesis: verum
end;
hence { f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X) ; :: thesis: verum