let n be non zero Nat; 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); ( f is without_antipodals implies Sn1->Sn f is odd )
assume A1:
f is without_antipodals
; Sn1->Sn f is odd
set g = Sn1->Sn f;
let x, y be complex-valued Function; BORSUK_7:def 1 ( 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
; (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
; verum