let x, y be real-valued FinSequence; ( len x = len y implies |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2) )
assume A1:
len x = len y
; |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)
|.(x - y).| ^2 =
|((x - y),(x - y))|
by Th4
.=
(|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
by A1, RVSUM_1:129
.=
((|.x.| ^2) - (2 * |(y,x)|)) + |(y,y)|
by Th4
.=
((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)
by Th4
;
hence
|.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)
; verum