let L be non empty addLoopStr ; :: thesis: ( L is Abelian & L is right_zeroed implies L is left_zeroed )
assume that
A1: L is Abelian and
A2: L is right_zeroed ; :: thesis: L is left_zeroed
let x be Element of L; :: according to ALGSTR_1:def 2 :: thesis: (0. L) + x = x
thus (0. L) + x = x + (0. L) by A1, RLVECT_1:def 2
.= x by A2, RLVECT_1:def 4 ; :: thesis: verum