let A, B, C, D be real number ; :: thesis: for h, g being Function of (TOP-REAL 2),(TOP-REAL 2) st A > 0 & C > 0 & h = AffineMap A,B,C,D & g = AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C)) holds
( g = h " & h = g " )
let h, g be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( A > 0 & C > 0 & h = AffineMap A,B,C,D & g = AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C)) implies ( g = h " & h = g " ) )
assume A1: ( A > 0 & C > 0 & h = AffineMap A,B,C,D & g = AffineMap (1 / A),(- (B / A)),(1 / C),(- (D / C)) ) ; :: thesis: ( g = h " & h = g " )
then A2: h is one-to-one by JGRAPH_2:54;
A3: 1 / A > 0 by A1, XREAL_1:141;
A4: 1 / C > 0 by A1, XREAL_1:141;
A5: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A6: dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
reconsider RA = A as Real by XREAL_0:def 1;
reconsider RB = B as Real by XREAL_0:def 1;
reconsider RC = C as Real by XREAL_0:def 1;
reconsider RD = D as Real by XREAL_0:def 1;
h = AffineMap RA,RB,RC,RD by A1;
then h is onto by A1, JORDAN1K:36;
then A7: rng h = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
g = AffineMap (1 / RA),(- (RB / RA)),(1 / RC),(- (RD / RC)) by A1;
then g is onto by A3, A4, JORDAN1K:36;
then A8: rng g = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
for x, y being set st x in dom h & y in dom g holds
( h . x = y iff g . y = x )

proof

let x, y be set ; :: thesis: ( x in dom h & y in dom g implies ( h . x = y iff g . y = x ) )
assume A9: ( x in dom h & y in dom g ) ; :: thesis: ( h . x = y iff g . y = x )
then reconsider px = x as Point of (TOP-REAL 2) ;
reconsider py = y as Point of (TOP-REAL 2) by A9;
A10: ( h . x = y implies g . y = x )

proof

assume A11: h . x = y ; :: thesis: g . y = x
h . px = |[((A * (px `1 )) + B),((C * (px `2 )) + D)]| by A1, JGRAPH_2:def 2;
then A12: ( py `1 = (A * (px `1 )) + B & py `2 = (C * (px `2 )) + D ) by A11, EUCLID:56;
A13: g . py = |[(((1 / A) * (py `1 )) + (- (B / A))),(((1 / C) * (py `2 )) + (- (D / C)))]| by A1, JGRAPH_2:def 2;
A14: ((1 / A) * (py `1 )) + (- (B / A)) = ((((1 / A) * A) * (px `1 )) + ((1 / A) * B)) + (- (B / A)) by A12
.= ((1 * (px `1 )) + ((1 / A) * B)) + (- (B / A)) by A1, XCMPLX_1:107
.= ((px `1 ) + (B / A)) + (- (B / A)) by XCMPLX_1:100
.= px `1 ;
((1 / C) * (py `2 )) + (- (D / C)) = ((((1 / C) * C) * (px `2 )) + ((1 / C) * D)) + (- (D / C)) by A12
.= ((1 * (px `2 )) + ((1 / C) * D)) + (- (D / C)) by A1, XCMPLX_1:107
.= ((px `2 ) + (D / C)) + (- (D / C)) by XCMPLX_1:100
.= px `2 ;
hence g . y = x by A13, A14, EUCLID:57; :: thesis: verum

end;

( g . y = x implies h . x = y )

proof

assume A15: g . y = x ; :: thesis: h . x = y
g . py = |[(((1 / A) * (py `1 )) + (- (B / A))),(((1 / C) * (py `2 )) + (- (D / C)))]| by A1, JGRAPH_2:def 2;
then A16: ( px `1 = ((1 / A) * (py `1 )) + (- (B / A)) & px `2 = ((1 / C) * (py `2 )) + (- (D / C)) ) by A15, EUCLID:56;
A17: h . px = |[((A * (px `1 )) + B),((C * (px `2 )) + D)]| by A1, JGRAPH_2:def 2;
A18: (A * (px `1 )) + B = (((A * (1 / A)) * (py `1 )) + (A * (- (B / A)))) + B by A16
.= ((1 * (py `1 )) + (A * (- (B / A)))) + B by A1, XCMPLX_1:107
.= ((py `1 ) + (A * ((- B) / A))) + B by XCMPLX_1:188
.= ((py `1 ) + (- B)) + B by A1, XCMPLX_1:88
.= py `1 ;
(C * (px `2 )) + D = (((C * (1 / C)) * (py `2 )) + (C * (- (D / C)))) + D by A16
.= ((1 * (py `2 )) + (C * (- (D / C)))) + D by A1, XCMPLX_1:107
.= ((py `2 ) + (C * ((- D) / C))) + D by XCMPLX_1:188
.= ((py `2 ) + (- D)) + D by A1, XCMPLX_1:88
.= py `2 ;
hence h . x = y by A17, A18, EUCLID:57; :: thesis: verum

end;

hence ( h . x = y iff g . y = x ) by A10; :: thesis: verum

end;

then g = h " by A2, A5, A6, A7, A8, FUNCT_1:60;
hence ( g = h " & h = g " ) by A2, FUNCT_1:65; :: thesis: verum