let K be non empty addLoopStr ; :: thesis: for a being Element of K holds - <*a*> = <*(- a)*>
let a be Element of K; :: thesis: - <*a*> = <*(- a)*>
thus - <*a*> = <*((comp K) . a)*> by FINSEQ_2:35
.= <*(- a)*> by VECTSP_1:def 13 ; :: thesis: verum