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