:: deftheorem defines Ortm ANALORT:def 1 :
for V being RealLinearSpace
for x, y, u being VECTOR of V holds Ortm (x,y,u) = ((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y);