theorem Th1: :: ANALORT:1

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