let b be BinOp of COMPLEX; :: thesis: ( b = diffcomplex iff b = addcomplex * ((id COMPLEX),compcomplex) )
now :: thesis: for c1, c2 being Element of COMPLEX holds diffcomplex . (c1,c2) = (addcomplex * ((id COMPLEX),compcomplex)) . (c1,c2)
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:82 ; :: thesis: verum
end;
hence ( b = diffcomplex iff b = addcomplex * ((id COMPLEX),compcomplex) ) by BINOP_1:2; :: thesis: verum