theorem Th7: :: MORPH_01:7

for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }