let n be non zero Nat; :: thesis: for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)
for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds
(f . x) - (f . (- x)) <> 0. (TOP-REAL n)
set TC4 = Tcircle ((0. (TOP-REAL (n + 1))),1);
let f be Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n); :: thesis: for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds
(f . x) - (f . (- x)) <> 0. (TOP-REAL n)
let x be Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)); :: thesis: ( f is without_antipodals implies (f . x) - (f . (- x)) <> 0. (TOP-REAL n) )
assume A1: f is without_antipodals ; :: thesis: (f . x) - (f . (- x)) <> 0. (TOP-REAL n)
A2: dom f = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by FUNCT_2:def 1;
reconsider y = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
reconsider a = x, b = y as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider x1 = x as Point of (TOP-REAL (n + 1)) by PRE_TOPC:25;
assume A3: (f . x) - (f . (- x)) = 0. (TOP-REAL n) ; :: thesis: contradiction
x1, - x1 are_antipodals_of 0. (TOP-REAL (n + 1)),1,f
proof
thus x1, - x1 are_antipodals_of 0. (TOP-REAL (n + 1)),1 by Th54; :: according to BORSUK_7:def 12 :: thesis: ( x1 in dom f & - x1 in dom f & f . x1 = f . (- x1) )
( f . x = f . a & f . y = f . b ) ;
hence ( x1 in dom f & - x1 in dom f ) by A2; :: thesis: f . x1 = f . (- x1)
(f . a) - (f . y) = 0. (TOP-REAL n) by A3;
hence f . x1 = f . (- x1) by RLVECT_1:21; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum