theorem Th22: :: JGRAPH_4:22

for sn being Real
for K1 being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K1),R^1 st - 1 < sn & ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = |.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) ) ) holds
f is continuous