let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for u, w being Element of V holds - (u + w) = (- w) + (- u)
let u, w be Element of V; :: thesis: - (u + w) = (- w) + (- u)
(u + w) + ((- w) + (- u)) = u + (w + ((- w) + (- u))) by Def3
.= u + ((w + (- w)) + (- u)) by Def3
.= u + ((0. V) + (- u)) by Def10
.= 0. V by Def10 ;
hence - (u + w) = (- w) + (- u) by Def10; :: thesis: verum