let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v being Element of V st v + v = 0. V holds
v = 0. V
let v be Element of V; :: thesis: ( v + v = 0. V implies v = 0. V )
assume v + v = 0. V ; :: thesis: v = 0. V
then v = - v by Def10;
hence v = 0. V by Th19; :: thesis: verum