theorem Th34: :: JORDAN1K:34

for s1, s2, t1, t2 being Real st s1 > 0 & s2 > 0 holds
(AffineMap (s1,t1,s2,t2)) * (AffineMap ((1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2)))) = id (REAL 2)