:: deftheorem Def5 defines stereographic_projection MFOLD_2:def 5 :
for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st p in Sphere ((0. (TOP-REAL n)),1) holds
for b₄ being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds
( b₄ = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds
b₄ . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) );