theorem :: COMPLSP2:76

for x, y being FinSequence of COMPLEX st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|