let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1 st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
let V1 be finite-dimensional VectSp of K; :: thesis: for R1, R2 being FinSequence of V1 st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be FinSequence of V1; :: 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 reconsider r1 = R1, r2 = R2 as Element of (len R1) -tuples_on the carrier of V1 by FINSEQ_2:92;
thus Sum (R1 + R2) = Sum (r1 + r2)
.= (Sum R1) + (Sum R2) by FVSUM_1:76 ; :: thesis: verum