for a, b being Real
for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))