let A, B, C, D be real number ; :: thesis: for h being Function of (TOP-REAL 2),(TOP-REAL 2) st A > 0 & C > 0 & h = AffineMap A,B,C,D holds
( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2 ) )
let h be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( A > 0 & C > 0 & h = AffineMap A,B,C,D implies ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2 ) ) )
assume A1: ( A > 0 & C > 0 & h = AffineMap A,B,C,D ) ; :: thesis: ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2 ) )
then A2: h is one-to-one by JGRAPH_2:54;
A3: dom h = [#] (TOP-REAL 2) by FUNCT_2:def 1;
set g = AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C));
A4: dom (AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C))) = [#] (TOP-REAL 2) by FUNCT_2:def 1;
A5: AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C)) = h " by A1, Th49;
then A6: rng h = [#] (TOP-REAL 2) by A2, A4, FUNCT_1:54;
then A7: h /" is continuous by A1, A5, JGRAPH_2:54, TOPS_2:def 4;
for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2

proof

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `2 < p2 `2 implies (h . p1) `2 < (h . p2) `2 )
assume A8: p1 `2 < p2 `2 ; :: thesis: (h . p1) `2 < (h . p2) `2
A9: h . p1 = |[((A * (p1 `1 )) + B),((C * (p1 `2 )) + D)]| by A1, JGRAPH_2:def 2;
A10: h . p2 = |[((A * (p2 `1 )) + B),((C * (p2 `2 )) + D)]| by A1, JGRAPH_2:def 2;
A11: (h . p1) `2 = (C * (p1 `2 )) + D by A9, EUCLID:56;
A12: (h . p2) `2 = (C * (p2 `2 )) + D by A10, EUCLID:56;
C * (p1 `2 ) < C * (p2 `2 ) by A1, A8, XREAL_1:70;
hence (h . p1) `2 < (h . p2) `2 by A11, A12, XREAL_1:10; :: thesis: verum

end;

hence ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2 ) ) by A1, A2, A3, A6, A7, TOPS_2:def 5; :: thesis: verum