let a, b be Real; :: thesis: for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))
let s, t be Point of (TOP-REAL 2); :: thesis: ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))
thus ((a * s) + (b * t)) `2 = ((a * s) `2) + ((b * t) `2) by TOPREAL3:2
.= (a * (s `2)) + ((b * t) `2) by TOPREAL3:4
.= (a * (s `2)) + (b * (t `2)) by TOPREAL3:4 ; :: thesis: verum