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 Th4
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, RVSUM_1:128
.= ((|.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) ; :: thesis: verum