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