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 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) )
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 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) ) )
assume that
A1: A > 0 and
A2: C > 0 and
A3: h = AffineMap A,B,C,D ; :: thesis: ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) )
A4: h is one-to-one by A1, A2, A3, JGRAPH_2:54;
set g = AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C));
A5: AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C)) = h " by A1, A2, A3, Th49;
A6: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1

proof

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

end;

A9: dom h = [#] (TOP-REAL 2) by FUNCT_2:def 1;
dom (AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C))) = [#] (TOP-REAL 2) by FUNCT_2:def 1;
then A10: rng h = [#] (TOP-REAL 2) by A4, A5, FUNCT_1:54;
then h /" is continuous by A1, A2, A3, A5, JGRAPH_2:54, TOPS_2:def 4;
hence ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) ) by A3, A4, A9, A10, A6, TOPS_2:def 5; :: thesis: verum