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 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:54;
A6: 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 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:56;
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:107
.= ((px `1 ) + (B / A)) + (- (B / A)) by XCMPLX_1:100
.= px `1 ;
py `2 = (C * (px `2 )) + D by A10, A11, EUCLID:56;
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:107
.= ((px `2 ) + (D / C)) + (- (D / C)) by XCMPLX_1:100
.= 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:57; :: 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:56;
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:107
.= ((py `1 ) + (A * ((- B) / A))) + B by XCMPLX_1:188
.= ((py `1 ) + (- B)) + B by A1, XCMPLX_1:88
.= py `1 ;
px `2 = ((1 / C) * (py `2 )) + (- (D / C)) by A14, A15, EUCLID:56;
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:107
.= ((py `2 ) + (C * ((- D) / C))) + D by XCMPLX_1:188
.= ((py `2 ) + (- D)) + D by A2, XCMPLX_1:88
.= 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:57; :: 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 by XREAL_0:def 1;
reconsider RC = C as Real by XREAL_0:def 1;
reconsider RB = B as Real by XREAL_0:def 1;
reconsider RA = A as Real by XREAL_0:def 1;
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:141;
1 / A > 0 by A1, XREAL_1:141;
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:60;
hence ( g = h " & h = g " ) by A5, FUNCT_1:65; :: thesis: verum