theorem :: RVSUM_1:125

for x, y being Real
for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)