let x be Element of (TOP-REAL 1); :: thesis: for a, r being Real st x = <*a*> holds
r * x = <*(r * a)*>
let a, r be Real; :: thesis: ( x = <*a*> implies r * x = <*(r * a)*> )
assume x = <*a*> ; :: thesis: r * x = <*(r * a)*>
then A1: x . 1 = a by FINSEQ_1:def 8;
reconsider x9 = x as Element of REAL 1 by EUCLID:22;
A2: (r * x9) . 1 = r * (x . 1) by RVSUM_1:44;
r * x9 in REAL 1 ;
then r * x is Element of (TOP-REAL 1) by EUCLID:22;
then consider b being Real such that
A3: r * x = <*b*> by JORDAN2B:20;
thus r * x = <*(r * a)*> by A1, A3, A2, FINSEQ_1:def 8; :: thesis: verum