for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of V holds (u # u1) # (v # v1) = (u # v) # (u1 # v1)