theorem Th2: :: MATHMORP:2

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T holds {(0. T)} + x = {x}