let P, Q be set ; :: thesis: for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q
let f be Function of P,Q; :: thesis: {f} is FUNCTION_DOMAIN of P,Q
for g being Element of {f} holds g is Function of P,Q by TARSKI:def 1;
hence {f} is FUNCTION_DOMAIN of P,Q by Def12; :: thesis: verum