for P, Q being set
for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q