let X be RealLinearSpace; :: thesis: for R1, R2 being FinSequence of X st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be FinSequence of X; :: thesis: ( len R1 = len R2 implies Sum (R1 + R2) = (Sum R1) + (Sum R2) )
assume len R1 = len R2 ; :: thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2)
then dom R1 = dom R2 by FINSEQ_3:29;
hence Sum (R1 + R2) = (Sum R1) + (Sum R2) by BINOM:7; :: thesis: verum