for S, T being Element of REAL 2 holds Sum (sqr (T - S)) = Sum (sqr (S - T))