let x, y, a be Real; :: thesis: for vx being Element of REAL 2 st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>
let vx be Element of REAL 2; :: thesis: ( vx = <*x,y*> implies a * vx = <*(a * x),(a * y)*> )
reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;
assume vx = <*x,y*> ; :: thesis: a * vx = <*(a * x),(a * y)*>
hence a * vx = <*((a multreal) . x1),((a multreal) . y1)*> by FINSEQ_2:36
.= <*(a * x1),((a multreal) . y1)*> by RVSUM_1:5
.= <*(a * x),(a * y)*> by RVSUM_1:5 ;
:: thesis: verum