theorem Th3: :: ANALOAF:3

for V being RealLinearSpace
for u, v being VECTOR of V
for a being Real holds a * (u - v) = - (a * (v - u))