theorem :: COMPLSP2:77

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)|