let K be Field; :: thesis: for V1 being finite-dimensional VectSp of finite-dimensional
for R1, R2 being FinSequence of st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
let V1 be finite-dimensional VectSp of finite-dimensional ; :: thesis: for R1, R2 being FinSequence of st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be FinSequence of ; :: 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:110;
thus Sum (R1 + R2) = Sum (r1 + r2)
.= (Sum R1) + (Sum R2) by FVSUM_1:95 ; :: thesis: verum