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