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