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