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