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