let b be BinOp of COMPLEX ; :: thesis: ( b = diffcomplex iff b = addcomplex * (id COMPLEX ),compcomplex )

now

let c1, c2 be Element of COMPLEX ; :: thesis: diffcomplex . c1,c2 = (addcomplex * (id COMPLEX ),compcomplex ) . c1,c2
thus diffcomplex . c1,c2 = c1 - c2 by BINOP_2:def 4
.= c1 + (- c2)
.= addcomplex . c1,(- c2) by BINOP_2:def 3
.= addcomplex . c1,(compcomplex . c2) by BINOP_2:def 1
.= (addcomplex * (id COMPLEX ),compcomplex ) . c1,c2 by FINSEQOP:87 ; :: thesis: verum

end;

hence ( b = diffcomplex iff b = addcomplex * (id COMPLEX ),compcomplex ) by BINOP_1:2; :: thesis: verum