let S, T be Element of REAL 2; :: thesis: Sum (sqr (T - S)) = Sum (sqr (S - T))
Sum (sqr (T - S)) = |.(T - S).| ^2 by TOPREAL9:5
.= |.(S - T).| ^2 by EUCLID:18 ;
hence Sum (sqr (T - S)) = Sum (sqr (S - T)) by TOPREAL9:5; :: thesis: verum