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 Th10
.= (((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)) - (((|.x.| ^2) - (2 * |(y,x)|)) + (|.y.| ^2)) by A1, Th11
.= 4 * |(x,y)| ;
hence (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| ; :: thesis: verum