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