theorem Th65: :: JGRAPH_7:65

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