set IT = { x where x is Element of Funcs the carrier of P,the carrier of Q : ex f being continuous Function of P,Q st f = x } ;
not { x where x is Element of Funcs the carrier of P,the carrier of Q : ex f being continuous Function of P,Q st f = x } is empty

proof

consider z being Element of Q;
reconsider f = P --> z as continuous Function of P,Q by Thcontinuous02;
f is Element of Funcs the carrier of P,the carrier of Q by FUNCT_2:11;
then f in { x where x is Element of Funcs the carrier of P,the carrier of Q : ex f being continuous Function of P,Q st f = x } ;
hence not { x where x is Element of Funcs the carrier of P,the carrier of Q : ex f being continuous Function of P,Q st f = x } is empty ; :: thesis: verum

end;

hence { x where x is Element of Funcs the carrier of P,the carrier of Q : ex f being continuous Function of P,Q st f = x } is non empty set ; :: thesis: verum