( dom (A --> d) = A & rng (A --> d) c= {d} ) by FUNCOP_1:13;
hence A --> d is Element of Funcs (A,D) by FUNCT_2:def 2; :: thesis: verum