let n be non zero Nat; :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) st f is without_antipodals & f is continuous holds
Sn1->Sn f is continuous
set T = Tcircle ((0. (TOP-REAL (n + 1))),1);
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); :: thesis: ( f is without_antipodals & f is continuous implies Sn1->Sn f is continuous )
assume that
A1: f is without_antipodals and
A2: f is continuous ; :: thesis: Sn1->Sn f is continuous
set B = Sn1->Sn f;
reconsider g = f (-) as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:61;
reconsider B1 = f <--> g as Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:40;
set B2 = (n NormF) * B1;
A3: dom g = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def 1;
A4: dom B1 = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def 1;

A5: now :: thesis: for t being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) holds ((n NormF) * B1) . t = |.(B1 . t).|

let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); :: thesis: ((n NormF) * B1) . t = |.(B1 . t).|
thus ((n NormF) * B1) . t = (n NormF) . (B1 . t) by FUNCT_2:15
.= |.(B1 . t).| by JGRAPH_4:def 1 ; :: thesis: verum

end;

A6: now :: thesis: for t being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) holds |.(B1 . t).| <> 0

let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); :: thesis: |.(B1 . t).| <> 0
A7: B1 . t = (f . t) - (g . t) by A4, VALUED_2:def 46
.= (f . t) - (f . (- t)) by A3, VALUED_2:def 34 ;
(f . t) - (f . (- t)) <> 0. (TOP-REAL n) by A1, Th56;
hence |.(B1 . t).| <> 0 by A7, TOPRNS_1:24; :: thesis: verum

end;

A8: (n NormF) * B1 is non-empty

proof

let x be object ; :: according to FUNCT_1:def 9 :: thesis: ( not x in dom ((n NormF) * B1) or not ((n NormF) * B1) . x is empty )
assume x in dom ((n NormF) * B1) ; :: thesis: not ((n NormF) * B1) . x is empty
then reconsider x = x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
((n NormF) * B1) . x = |.(B1 . x).| by A5;
hence not ((n NormF) * B1) . x is empty by A6; :: thesis: verum

end;

A9: g is continuous Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by A2, TOPREALC:62;
B1 </> ((n NormF) * B1) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n) by TOPREALC:46;
hence Sn1->Sn f is continuous by A1, Th58, A8, A2, A9, TOPMETR:6; :: thesis: verum