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)*> )
assume A1: vx = <*x,y*> ; :: thesis: a * vx = <*(a * x),(a * y)*>
reconsider x1 = x, y1 = y as Element of REAL ;
thus a * vx = <*((a multreal ) . x1),((a multreal ) . y1)*> by A1, FINSEQ_2:40
.= <*(a * x1),((a multreal ) . y1)*> by RVSUM_1:19
.= <*(a * x),(a * y)*> by RVSUM_1:19 ; :: thesis: verum