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:158
.= ((|.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