let K be Field; :: 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: a1 = - a2 ; :: thesis: - a1 = a2
a1 + a2 = 0. K by A1, VECTSP_1:16;
hence - a1 = a2 by VECTSP_1:16; :: thesis: verum