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