let x, y be FinSequence of COMPLEX ; ( len x = len y implies |((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)| )
set z = |(x,y)|;
assume
len x = len y
; |((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|
then |((x - y),(x - y))| =
((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)|
by Th63
.=
((|(x,x)| - |(x,y)|) - (|(x,y)| *')) + |(y,y)|
by Th64
.=
(|(x,x)| - (|(x,y)| + (|(x,y)| *'))) + |(y,y)|
.=
(|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|
by Th20
;
hence
|((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|
; verum