let a, b be real number ; :: 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:7
.= (a * (s `1 )) + ((b * t) `1 ) by TOPREAL3:9
.= (a * (s `1 )) + (b * (t `1 )) by TOPREAL3:9 ; :: thesis: verum