let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| )
assume A1: len x = len y ; :: thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|
set z = |(x,y)|;
|((x + y),(x + y))| = ((|(x,x)| + |(x,y)|) + |(y,x)|) + |(y,y)| by A1, Th73
.= ((|(x,x)| + |(x,y)|) + (|(x,y)| *' )) + |(y,y)| by A1, Th75
.= (|(x,x)| + (|(x,y)| + (|(x,y)| *' ))) + |(y,y)|
.= (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| by Th24 ;
hence |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| ; :: thesis: verum