for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds (A (+) B) (+) C = A (+) (B (+) C) by Th10;