let V be RealLinearSpace; :: thesis: for u, x, y being VECTOR of V
for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
let u, x, y be VECTOR of V; :: thesis: for n being Real st Gen x,y holds
Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
let n be Real; :: thesis: ( Gen x,y implies Ortm (x,y,(n * u)) = n * (Ortm (x,y,u)) )
assume A1: Gen x,y ; :: thesis: Ortm (x,y,(n * u)) = n * (Ortm (x,y,u))
hence Ortm (x,y,(n * u)) = ((n * (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,(n * u)))) * y) by Lm7
.= ((n * (pr1 (x,y,u))) * x) + ((- (n * (pr2 (x,y,u)))) * y) by A1, Lm7
.= ((n * (pr1 (x,y,u))) * x) + ((n * (pr2 (x,y,u))) * (- y)) by RLVECT_1:24
.= ((n * (pr1 (x,y,u))) * x) + (- ((n * (pr2 (x,y,u))) * y)) by RLVECT_1:25
.= ((n * (pr1 (x,y,u))) * x) + (- (n * ((pr2 (x,y,u)) * y))) by RLVECT_1:def 7
.= ((n * (pr1 (x,y,u))) * x) + (n * (- ((pr2 (x,y,u)) * y))) by RLVECT_1:25
.= (n * ((pr1 (x,y,u)) * x)) + (n * (- ((pr2 (x,y,u)) * y))) by RLVECT_1:def 7
.= n * (((pr1 (x,y,u)) * x) + (- ((pr2 (x,y,u)) * y))) by RLVECT_1:def 5
.= n * (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * (- y))) by RLVECT_1:25
.= n * (Ortm (x,y,u)) by RLVECT_1:24 ;
:: thesis: verum