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 holds
Sn1->Sn f is odd
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: ( f is without_antipodals implies Sn1->Sn f is odd )
assume A1: f is without_antipodals ; :: thesis: Sn1->Sn f is odd
set g = Sn1->Sn f;
let x, y be complex-valued Function; :: according to BORSUK_7:def 1 :: thesis: ( x in dom (Sn1->Sn f) & - x in dom (Sn1->Sn f) & y = (Sn1->Sn f) . x implies (Sn1->Sn f) . (- x) = - y )
assume that
A2: x in dom (Sn1->Sn f) and
A3: - x in dom (Sn1->Sn f) and
A4: y = (Sn1->Sn f) . x ; :: thesis: (Sn1->Sn f) . (- x) = - y
reconsider b = - x as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A3;
reconsider a = - b as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by A2;
set p = (f . b) - (f . a);
set q = (f . a) - (f . b);
A5: (f . b) - (f . a) = - ((f . a) - (f . b)) by RLVECT_1:33;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A6: - ((f . b) - (f . a)) <> 0. (TOP-REAL n) by A1, Th56, Th14;
thus (Sn1->Sn f) . (- x) = Rn->S1 ((f . b) - (f . a)) by Def9
.= ((f . b) - (f . a)) (/) |.((f . b) - (f . a)).| by A1, Th56, Def8
.= ((f . b) - (f . a)) (/) |.(- ((f . a) - (f . b))).| by RLVECT_1:33
.= (- ((f . a) - (f . b))) (/) |.(- ((f . a) - (f . b))).| by RLVECT_1:33
.= - (((f . a) - (f . b)) (/) |.(- ((f . a) - (f . b))).|) by VALUED_2:30
.= - (((f . a) - (f . b)) (/) |.((f . a) - (f . b)).|) by TOPRNS_1:26
.= - (Rn->S1 ((f . a) - (f . b))) by A5, A6, Def8
.= - y by A4, Def9 ; :: thesis: verum