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