let X be RealNormSpace; :: thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds

Sum R3 = (Sum R1) + (Sum R2)

let R1, R2, R3 be FinSequence of X; :: thesis: ( len R1 = len R2 & R3 = R1 + R2 implies Sum R3 = (Sum R1) + (Sum R2) )

assume A1: ( len R1 = len R2 & R3 = R1 + R2 ) ; :: thesis: Sum R3 = (Sum R1) + (Sum R2)

then dom R1 = dom R2 by FINSEQ_3:29;

hence Sum R3 = (Sum R1) + (Sum R2) by A1, BINOM:7; :: thesis: verum

Sum R3 = (Sum R1) + (Sum R2)

let R1, R2, R3 be FinSequence of X; :: thesis: ( len R1 = len R2 & R3 = R1 + R2 implies Sum R3 = (Sum R1) + (Sum R2) )

assume A1: ( len R1 = len R2 & R3 = R1 + R2 ) ; :: thesis: Sum R3 = (Sum R1) + (Sum R2)

then dom R1 = dom R2 by FINSEQ_3:29;

hence Sum R3 = (Sum R1) + (Sum R2) by A1, BINOM:7; :: thesis: verum