theorem Th62: :: JGRAPH_7:62

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, I being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & a <= (f . O) `1 & (f . O) `1 < (f . I) `1 & (f . I) `1 <= b holds
( - 1 <= ((h * f) . O) `1 & ((h * f) . O) `1 < ((h * f) . I) `1 & ((h * f) . I) `1 <= 1 )