set f = A --> b;
A1: dom (A --> b) = A by FUNCOP_1:13;
thus A --> b is Function of A,B by A1; :: thesis: verum