let X be RealNormSpace; :: thesis: for R1, R2 being FinSequence of X
for a being Real st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let R1, R2 be FinSequence of X; :: thesis: for a being Real st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)
let a be 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;
A3: 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 A4: k in dom R2 by A1, VFUNCT_1:def 4;
thus R2 . k = R2 /. k by A4, PARTFUN1:def 6
.= a * (R1 /. k) by A4, A1, VFUNCT_1:def 4 ; :: thesis: verum

end;

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