let V1 be Field; :: 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

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