let F be non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr ; :: thesis: for a being Element of F holds a |^ 2 = (- a) |^ 2
let a be Element of F; :: thesis: a |^ 2 = (- a) |^ 2
set a2 = - a;
thus a |^ 2 = a * a by GROUP_1:51
.= (- a) * (- a) by VECTSP_1:10
.= (- a) |^ 2 by GROUP_1:51 ; :: thesis: verum