let d be real number ; :: thesis: compreal . d = (- 1) * d
d is Real by XREAL_0:def 1;
hence compreal . d = - d by BINOP_2:def 7
.= (- 1) * d ;
:: thesis: verum