for N being non zero Nat
for F being Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)) st ( for i being Nat st i in dom F holds
F . i = PROJ ((N + 1),i) ) holds
( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds
( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds
H is being_homeomorphism ) ) ) )