let d be Real; :: thesis: compreal . d = (- 1) * d
thus compreal . d = - d by BINOP_2:def 7
.= (- 1) * d ; :: thesis: verum