(- <*(- a),b,c*>) . 1 = - (<*(- a),b,c*> . 1) by VALUED_1:8
.= - (- a) ;
hence (- <*(- a),b,c*>) . 1 = a ; :: thesis: verum