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