theorem Th12: :: ANALORT:12

for V being RealLinearSpace
for u, x, y being VECTOR of V
for n being Real st Gen x,y holds
Orte (x,y,(n * u)) = n * (Orte (x,y,u))