theorem Th17: :: MORPH_01:17

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) )