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 2 :: 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 EUCLID:44;
A6: n in NAT by ORDINAL1:def 12;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A7: - ((f . b) - (f . a)) <> 0. (TOP-REAL n) by A1, Th66, Th15;
thus (Sn1->Sn f) . (- x) = Rn->S1 ((f . b) - (f . a)) by Def10
.= ((f . b) - (f . a)) (/) |.((f . b) - (f . a)).| by A1, Th66, Def9
.= ((f . b) - (f . a)) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44
.= (- ((f . a) - (f . b))) (/) |.(- ((f . a) - (f . b))).| by EUCLID:44
.= - (((f . a) - (f . b)) (/) |.(- ((f . a) - (f . b))).|) by VALUED_2:30
.= - (((f . a) - (f . b)) (/) |.((f . a) - (f . b)).|) by A6, TOPRNS_1:26
.= - (Rn->S1 ((f . a) - (f . b))) by A5, A7, Def9
.= - y by A4, Def10 ; :: thesis: verum