set g = A --> f;
dom (A --> f) = A by Th19;
A --> f is Function-yielding

proof

let a be set ; :: according to FUNCOP_1:def 6 :: thesis: ( a in dom (A --> f) implies (A --> f) . a is Function )
assume a in dom (A --> f) ; :: thesis: (A --> f) . a is Function
hence (A --> f) . a is Function by Th13; :: thesis: verum

end;

hence A --> f is Function-yielding ; :: thesis: verum