let A be non empty set ; :: thesis: CPFuncZero A <> CPFuncUnit A
(CPFuncUnit A) . the Element of A = 1 by COMPLEX1:def 4, FUNCOP_1:7;
hence CPFuncZero A <> CPFuncUnit A by FUNCOP_1:7; :: thesis: verum