theorem Th08: :: ANPROJ10:15

for V being RealLinearSpace
for P, Q being Element of V
for a, b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds
a = b