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