theorem rc: :: VECTSP13:33

for X being non empty set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Function of X,L holds f '+' ('-' f) = X --> (0. L)