theorem Th14: :: GROEB_3:14
for X being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Series of X,L holds (0_ (X,L)) - f = - f