(- 1) (#) (- f) = (- 1) (#) ((- 1) (#) f) by VALUED_1:def 6
.= ((- 1) * (- 1)) (#) f by VALUED_2:16 ;
hence (- 1) (#) (- f) = f ; :: thesis: verum