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