let p be Point of (TOP-REAL 2); :: thesis: for r, s1, s2 being Real holds (AffineMap r,s1,r,s2) . p = (r * p) + |[s1,s2]|
let r, s1, s2 be Real; :: thesis: (AffineMap r,s1,r,s2) . p = (r * p) + |[s1,s2]|
thus (AffineMap r,s1,r,s2) . p = |[((r * (p `1 )) + s1),((r * (p `2 )) + s2)]| by JGRAPH_2:def 2
.= |[(((r * p) `1 ) + s1),((r * (p `2 )) + s2)]| by TOPREAL3:9
.= |[(((r * p) `1 ) + s1),(((r * p) `2 ) + s2)]| by TOPREAL3:9
.= |[((r * p) `1 ),((r * p) `2 )]| + |[s1,s2]| by EUCLID:60
.= (r * p) + |[s1,s2]| by EUCLID:57 ; :: thesis: verum