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