let V be non empty right_complementable add-associative right_zeroed addLoopStr ; for v being Element of V holds
( v + (0. V) = v & (0. V) + v = v )
let v be Element of V; ( v + (0. V) = v & (0. V) + v = v )
consider w being Element of V such that
A1:
v + w = 0. V
by ALGSTR_0:def 11;
thus A2:
v + (0. V) = v
by Def7; (0. V) + v = v
w + v = 0. V
by A1, Lm1;
hence
(0. V) + v = v
by A2, A1, Def6; verum