theorem Th11: :: EUCLID_2:12

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