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

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