theorem Th54: :: JGRAPH_7:54

for a, b, c, d being Real
for h being Function of (TOP-REAL 2),(TOP-REAL 2)
for f being Function of I[01],(TOP-REAL 2)
for O being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . O) `1 = a holds
((h * f) . O) `1 = - 1