let LS be non empty addLoopStr ; :: thesis: ( the ZeroF of LS is_a_unity_wrt the addF of LS implies LS is right_zeroed )
assume A1: the ZeroF of LS is_a_unity_wrt the addF of LS ; :: thesis: LS is right_zeroed
let x be Element of LS; :: according to RLVECT_1:def 4 :: thesis: x + (0. LS) = x
thus x + (0. LS) = x by A1, BINOP_1:3; :: thesis: verum