let L be non empty addLoopStr ; :: thesis: ( L is zeroed implies L is right_zeroed )
assume L is zeroed ; :: thesis: L is right_zeroed
hence for v being Element of L holds v + (0. L) = v by Def16; :: according to RLVECT_1:def 4 :: thesis: verum