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