theorem :: RVSUM_1:128

for x, y being real-valued FinSequence st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|