let A be non empty set ; :: thesis: ComplexFuncZero A <> ComplexFuncUnit A

set a = the Element of A;

(ComplexFuncZero A) . the Element of A = 0c by FUNCOP_1:7;

hence ComplexFuncZero A <> ComplexFuncUnit A by COMPLEX1:def 4, FUNCOP_1:7; :: thesis: verum

set a = the Element of A;

(ComplexFuncZero A) . the Element of A = 0c by FUNCOP_1:7;

hence ComplexFuncZero A <> ComplexFuncUnit A by COMPLEX1:def 4, FUNCOP_1:7; :: thesis: verum