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