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