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 A1: R2 = a (#) R1 ; :: thesis: Sum R2 = a * (Sum R1)
dom R2 = dom R1 by A1, VFUNCT_1:def 4;
then A2: len R2 = len R1 by FINSEQ_3:29;
for k being Nat st k in dom R1 holds
R2 . k = a * (R1 /. k)

proof

let k be Nat; :: thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) )
assume k in dom R1 ; :: thesis: R2 . k = a * (R1 /. k)
then A3: k in dom R2 by A1, VFUNCT_1:def 4;
hence R2 . k = R2 /. k by PARTFUN1:def 6
.= a * (R1 /. k) by A3, A1, VFUNCT_1:def 4 ;
:: thesis: verum

end;

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