theorem Th24: :: MORPH_01:24
for E being RealLinearSpace
for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )