let A, B, C, D be Real; :: 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 that
A1: A > 0 and
A2: C > 0 and
A3: h = AffineMap (A,B,C,D) and
A4: g = AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))) ; :: thesis: ( g = h " & h = g " )
A5: h is one-to-one by A1, A2, A3, JGRAPH_2:44;
A6: for x, y being object st x in dom h & y in dom g holds
( h . x = y iff g . y = x )

proof

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

proof

assume A10: h . x = y ; :: thesis: g . y = x
A11: h . px = |[((A * (px `1)) + B),((C * (px `2)) + D)]| by A3, JGRAPH_2:def 2;
then py `1 = (A * (px `1)) + B by A10, EUCLID:52;
then A12: ((1 / A) * (py `1)) + (- (B / A)) = ((((1 / A) * A) * (px `1)) + ((1 / A) * B)) + (- (B / A))
.= ((1 * (px `1)) + ((1 / A) * B)) + (- (B / A)) by A1, XCMPLX_1:106
.= ((px `1) + (B / A)) + (- (B / A)) by XCMPLX_1:99
.= px `1 ;
py `2 = (C * (px `2)) + D by A10, A11, EUCLID:52;
then A13: ((1 / C) * (py `2)) + (- (D / C)) = ((((1 / C) * C) * (px `2)) + ((1 / C) * D)) + (- (D / C))
.= ((1 * (px `2)) + ((1 / C) * D)) + (- (D / C)) by A2, XCMPLX_1:106
.= ((px `2) + (D / C)) + (- (D / C)) by XCMPLX_1:99
.= px `2 ;
g . py = |[(((1 / A) * (py `1)) + (- (B / A))),(((1 / C) * (py `2)) + (- (D / C)))]| by A4, JGRAPH_2:def 2;
hence g . y = x by A12, A13, EUCLID:53; :: thesis: verum

end;

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

proof

assume A14: g . y = x ; :: thesis: h . x = y
A15: g . py = |[(((1 / A) * (py `1)) + (- (B / A))),(((1 / C) * (py `2)) + (- (D / C)))]| by A4, JGRAPH_2:def 2;
then px `1 = ((1 / A) * (py `1)) + (- (B / A)) by A14, EUCLID:52;
then A16: (A * (px `1)) + B = (((A * (1 / A)) * (py `1)) + (A * (- (B / A)))) + B
.= ((1 * (py `1)) + (A * (- (B / A)))) + B by A1, XCMPLX_1:106
.= ((py `1) + (A * ((- B) / A))) + B by XCMPLX_1:187
.= ((py `1) + (- B)) + B by A1, XCMPLX_1:87
.= py `1 ;
px `2 = ((1 / C) * (py `2)) + (- (D / C)) by A14, A15, EUCLID:52;
then A17: (C * (px `2)) + D = (((C * (1 / C)) * (py `2)) + (C * (- (D / C)))) + D
.= ((1 * (py `2)) + (C * (- (D / C)))) + D by A2, XCMPLX_1:106
.= ((py `2) + (C * ((- D) / C))) + D by XCMPLX_1:187
.= ((py `2) + (- D)) + D by A2, XCMPLX_1:87
.= py `2 ;
h . px = |[((A * (px `1)) + B),((C * (px `2)) + D)]| by A3, JGRAPH_2:def 2;
hence h . x = y by A16, A17, EUCLID:53; :: thesis: verum

end;

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

end;

A18: dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
reconsider RD = D as Real ;
reconsider RC = C as Real ;
reconsider RB = B as Real ;
reconsider RA = A as Real ;
A19: g = AffineMap ((1 / RA),(- (RB / RA)),(1 / RC),(- (RD / RC))) by A4;
h = AffineMap (RA,RB,RC,RD) by A3;
then h is onto by A1, A2, JORDAN1K:36;
then A20: rng h = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
A21: 1 / C > 0 by A2, XREAL_1:139;
1 / A > 0 by A1, XREAL_1:139;
then g is onto by A21, A19, JORDAN1K:36;
then A22: rng g = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then g = h " by A5, A18, A20, A22, A6, FUNCT_1:38;
hence ( g = h " & h = g " ) by A5, FUNCT_1:43; :: thesis: verum