let x, y be real-valued FinSequence; :: thesis: ( len x = len y implies (|.(x + y).| ^2 ) - (|.(x - y).| ^2 ) = 4 * |(x,y)| )
assume A1: len x = len y ; :: thesis: (|.(x + y).| ^2 ) - (|.(x - y).| ^2 ) = 4 * |(x,y)|
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
.= 4 * |(x,y)| ;
hence (|.(x + y).| ^2 ) - (|.(x - y).| ^2 ) = 4 * |(x,y)| ; :: thesis: verum