for n being non zero Nat
for f, g, B1 being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st g = f (-) & B1 = f <--> g & f is without_antipodals holds
Sn1->Sn f = B1 </> ((n NormF) * B1)