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