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