let K be Field; :: thesis: for a1, a2 being Element of K st a1 = - a2 holds
a1 |^ 2 = a2 |^ 2
let a1, a2 be Element of K; :: thesis: ( a1 = - a2 implies a1 |^ 2 = a2 |^ 2 )
assume A1: a1 = - a2 ; :: thesis: a1 |^ 2 = a2 |^ 2
thus a1 |^ 2 = a1 * a1 by GROUP_1:51
.= a2 * a2 by A1, EC_PF_1:26
.= a2 |^ 2 by GROUP_1:51 ; :: thesis: verum