for x, y being real-valued FinSequence st len x = len y holds
(|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|