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