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:25;
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

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:56;
p in the carrier of (TOP-REAL 2) ;
then A4: p in REAL 2 by EUCLID:25;
A5: s1 * (1 / s1) = 1 by A1, XCMPLX_1:107;
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:21
.= (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:56
.= |[((((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:88
.= |[(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:88
.= |[(p `1 ),(((1 * (p `2 )) - (1 * t2)) + t2)]| by A2, XCMPLX_1:107
.= p by EUCLID:57
.= f . p by A4, FUNCT_1:35 ; :: thesis: verum

end;

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