let s1, s2, t1, t2 be Real; ( 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
; (AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)
now 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 . plet p be
Point of
(TOP-REAL 2);
((AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))))) . p = f . pset 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
;
verum end;
hence
(AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)
by FUNCT_2:63; verum