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