let x, y be real-valued FinSequence; :: thesis: ( len x = len y implies |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| )
A1: (|(x,x)| + |(x,y)|) + |(x,y)| = |(x,x)| + (2 * |(x,y)|) ;
assume len x = len y ; :: thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
hence |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, Th126; :: thesis: verum