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:4
.= |[(((r * p) `1) + s1),(((r * p) `2) + s2)]| by TOPREAL3:4
.= |[((r * p) `1),((r * p) `2)]| + |[s1,s2]| by EUCLID:56
.= (r * p) + |[s1,s2]| by EUCLID:53 ; :: thesis: verum