A --> 1 is Function of A,REAL by FUNCOP_1:57;
hence A --> 1 is Element of Funcs (A,REAL) by FUNCT_2:11; :: thesis: verum