A --> 0 is Function of A,REAL by FUNCOP_1:45;
hence A --> 0 is Element of Funcs (A,REAL) by FUNCT_2:8; :: thesis: verum