let x, y, a be Real; :: thesis: for vx being Point of (REAL-NS 2) st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>
let vx be Point of (REAL-NS 2); :: thesis: ( vx = <*x,y*> implies a * vx = <*(a * x),(a * y)*> )
assume A1: vx = <*x,y*> ; :: thesis: a * vx = <*(a * x),(a * y)*>
reconsider vx1 = vx as Element of REAL 2 by REAL_NS1:def 4;
thus a * vx = a * vx1 by REAL_NS1:3
.= <*(a * x),(a * y)*> by A1, Lm8 ; :: thesis: verum