let X be RealLinearSpace; :: thesis: for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let R1, R2 be FinSequence of X; :: thesis: for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let a be Element of REAL ; :: thesis: ( R2 = a (#) R1 implies Sum R2 = a * (Sum R1) )
assume AS: R2 = a (#) R1 ; :: thesis: Sum R2 = a * (Sum R1)
dom R2 = dom R1 by VFUNCT_1:def 4, AS;
then P1: len R2 = len R1 by FINSEQ_3:31;
for k being Element of NAT st k in dom R1 holds
R2 . k = a * (R1 /. k)

proof

let k be Element of NAT ; :: thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) )
assume k in dom R1 ; :: thesis: R2 . k = a * (R1 /. k)
then P21: k in dom R2 by VFUNCT_1:def 4, AS;
hence R2 . k = R2 /. k by PARTFUN1:def 8
.= a * (R1 /. k) by P21, AS, VFUNCT_1:def 4 ;
:: thesis: verum

end;

hence Sum R2 = a * (Sum R1) by P1, RLVECT_2:5; :: thesis: verum