for E being RealLinearSpace
for A, B being binary-image of E holds A (+) B = union { (b + A) where b is Element of E : b in B }