let A be non empty set ; :: thesis: ComplexFuncZero A <> ComplexFuncUnit A
consider a being Element of A;
(ComplexFuncZero A) . a = 0c by FUNCOP_1:13;
hence ComplexFuncZero A <> ComplexFuncUnit A by COMPLEX1:def 7, FUNCOP_1:13; :: thesis: verum