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