let n be non zero Nat; :: thesis:
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:
assume that
A1: f is without_antipodals and
A2: f is continuous ; :: thesis:
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;

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

end;

let t be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); :: thesis:
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:

end;

let x be object ; :: according to FUNCT_1:def 9 :: thesis:
assume x in dom ((n NormF) * B1) ; :: thesis:
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:

end;