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)

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

thus
Sum R2 = a * (Sum R1)
by A2, A3, RLVECT_2:3; :: thesis: verum
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;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