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
set z = the Element of Q;
reconsider f = P --> the Element of Q as continuous Function of P,Q by Th7;
f is Element of Funcs ( the carrier of P, the carrier of Q) by FUNCT_2:8;
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