theorem :: EUCLID:20

for x, y being real-valued FinSequence holds sqr (x - y) = sqr (y - x)