set f = A --> b;
A1: dom (A --> b) = A by FUNCOP_1:19;
A2: rng (A --> b) = {b} by FUNCOP_1:14;
{b} c= B by ZFMISC_1:37;
hence A --> b is Element of Funcs A,B by A1, A2, FUNCT_2:def 2; :: thesis: verum