let V1 be free finite-rank Z_Module; :: thesis: for P1, P2 being FinSequence of V1 st len P1 = len P2 holds
Sum (P1 + P2) = (Sum P1) + (Sum P2)
let P1, P2 be FinSequence of V1; :: thesis: ( len P1 = len P2 implies Sum (P1 + P2) = (Sum P1) + (Sum P2) )
assume len P1 = len P2 ; :: thesis: Sum (P1 + P2) = (Sum P1) + (Sum P2)
then reconsider R1 = P1, R2 = P2 as Element of (len P1) -tuples_on the carrier of V1 by FINSEQ_2:92;
thus Sum (P1 + P2) = Sum (R1 + R2)
.= (Sum P1) + (Sum P2) by FVSUM_1:76 ; :: thesis: verum