theorem :: MATHMORP:6

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