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 Th65;
hence Funcs (P,B) is FUNCTION_DOMAIN of P,B by Def12; :: thesis: verum