A --> 0 is Function of A,REAL by FUNCOP_1:58;
hence A --> 0 is Element of PFuncs (A,REAL) by PARTFUN1:119; :: thesis: verum