let P be set ; :: thesis: for B being non empty set holds Funcs P,B is FUNCTION_DOMAIN of P,B
let B be non empty set ; :: thesis: Funcs P,B is FUNCTION_DOMAIN of P,B
for f being Element of Funcs P,B holds f is Function of P,B by Th121;
hence Funcs P,B is FUNCTION_DOMAIN of P,B by Def13; :: thesis: verum