theorem Th10: :: ANALORT:10

for V being RealLinearSpace
for u, v, x, y being VECTOR of V st Gen x,y holds
Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))