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