let q, p 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:57 ; :: thesis: verum