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