let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a1, a2 being Element of K st a1 = - a2 holds
- a1 = a2
let a1, a2 be Element of K; :: thesis: ( a1 = - a2 implies - a1 = a2 )
assume a1 = - a2 ; :: thesis: - a1 = a2
then a1 + a2 = 0. K by VECTSP_1:16;
hence - a1 = a2 by VECTSP_1:16; :: thesis: verum