let s1, s2, t1, t2 be Real; :: thesis: ( s1 > 0 & s2 > 0 implies (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) )
the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
then reconsider f = id (REAL 2) as Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) ;
assume that
A1: s1 > 0 and
A2: s2 > 0 ; :: thesis: (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)

now :: thesis: for p being Point of (TOP-REAL 2) holds ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = f . p

let p be Point of (TOP-REAL 2); :: thesis: ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = f . p
set q = |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]|;
A3: |[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2 = ((1 / s2) * (p `2)) - (t2 / s2) by EUCLID:52;
p in the carrier of (TOP-REAL 2) ;
then A4: p in REAL 2 by EUCLID:22;
A5: s1 * (1 / s1) = 1 by A1, XCMPLX_1:106;
thus ((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = (AffineMap (s1,t1,s2,t2)) . ((AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) . p) by FUNCT_2:15
.= (AffineMap (s1,t1,s2,t2)) . |[(((1 / s1) * (p `1)) + (- (t1 / s1))),(((1 / s2) * (p `2)) + (- (t2 / s2)))]| by JGRAPH_2:def 2
.= |[((s1 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by JGRAPH_2:def 2
.= |[((s1 * (((1 / s1) * (p `1)) - (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by EUCLID:52
.= |[((((s1 * (1 / s1)) * (p `1)) - (s1 * (t1 / s1))) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]|
.= |[(((1 * (p `1)) - (1 * t1)) + t1),((s2 * (|[(((1 / s1) * (p `1)) - (t1 / s1)),(((1 / s2) * (p `2)) - (t2 / s2))]| `2)) + t2)]| by A1, A5, XCMPLX_1:87
.= |[(p `1),(((s2 * ((1 / s2) * (p `2))) - (s2 * (t2 / s2))) + t2)]| by A3
.= |[(p `1),((((s2 * (1 / s2)) * (p `2)) - t2) + t2)]| by A2, XCMPLX_1:87
.= |[(p `1),(((1 * (p `2)) - (1 * t2)) + t2)]| by A2, XCMPLX_1:106
.= p by EUCLID:53
.= f . p by A4, FUNCT_1:18 ; :: thesis: verum

end;

hence (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2) by FUNCT_2:63; :: thesis: verum