let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real holds (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q
let r be Real; :: thesis: (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + q
thus (AffineMap (r,(q `1),r,(q `2))) . p = (r * p) + |[(q `1),(q `2)]| by Th32
.= (r * p) + q by EUCLID:53 ; :: thesis: verum