let A be non empty set ; :: thesis: RealPFuncZero A <> RealPFuncUnit A
set a = the Element of A;
(RealPFuncZero A) . the Element of A = 0 by FUNCOP_1:7;
hence RealPFuncZero A <> RealPFuncUnit A by FUNCOP_1:7; :: thesis: verum