let A, B, C, D be Real; :: 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 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 `2 < p2 `2 holds
(h . p1) `2 < (h . p2) `2 ) )
A4: h is one-to-one by A1, A2, A3, JGRAPH_2:44;
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 `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 )
h . p1 = |[((A * (p1 `1)) + B),((C * (p1 `2)) + D)]| by A3, JGRAPH_2:def 2;
then A7: (h . p1) `2 = (C * (p1 `2)) + D by EUCLID:52;
h . p2 = |[((A * (p2 `1)) + B),((C * (p2 `2)) + D)]| by A3, JGRAPH_2:def 2;
then A8: (h . p2) `2 = (C * (p2 `2)) + D by EUCLID:52;
assume p1 `2 < p2 `2 ; :: thesis: (h . p1) `2 < (h . p2) `2
then C * (p1 `2) < C * (p2 `2) by A2, XREAL_1:68;
hence (h . p1) `2 < (h . p2) `2 by A7, A8, XREAL_1:8; :: 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:32;
then ( h is onto & h is one-to-one ) by A1, A2, A3, FUNCT_2:def 3, JGRAPH_2:44;
then h /" is continuous by A5, TOPS_2:def 4;
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 A3, A4, A9, A10, A6, TOPS_2:def 5; :: thesis: verum