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