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