let L be non empty addLoopStr ; :: thesis: ( L is Abelian & L is right_zeroed implies L is zeroed )
assume A1: ( L is Abelian & L is right_zeroed ) ; :: thesis: L is zeroed
let a be Element of L; :: according to RLVECT_1:def 13 :: thesis: ( a + (0. L) = a & (0. L) + a = a )
thus a + (0. L) = a by A1; :: thesis: (0. L) + a = a
hence (0. L) + a = a by A1; :: thesis: verum