let f be Function of (Tcircle (p,r)),(TOP-REAL 2); ( f is continuous implies f is with_antipodals )
assume A1:
f is continuous
; f is with_antipodals
A2:
dom f = the carrier of (Tcircle (p,r))
by FUNCT_2:def 1;
per cases
( r is positive or r is zero )
;
suppose
r is
positive
;
f is with_antipodals then reconsider r1 =
r as
positive Real ;
reconsider f1 =
f as
continuous Function of
(Tcircle (p,r1)),
(TOP-REAL 2) by A1;
reconsider h =
CircleIso (
p,
r1) as
Function of
(Tcircle ((0. (TOP-REAL 3)),1)),
(Tcircle (p,r1)) ;
f1 * h is
with_antipodals
by Lm21;
then consider x,
y being
Point of
(TOP-REAL 3) such that A3:
x,
y are_antipodals_of 0. (TOP-REAL 3),1,
f1 * h
;
A4:
x in dom (f * h)
by A3;
A5:
y in dom (f * h)
by A3;
A6:
(f * h) . x = (f * h) . y
by A3;
(
h . x is
Point of
(Tcircle (p,r1)) &
h . y is
Point of
(Tcircle (p,r1)) )
by A4, A5, FUNCT_2:5;
then reconsider hx =
h . x,
hy =
h . y as
Point of
(TOP-REAL 3) by PRE_TOPC:25;
take
hx
;
BORSUK_7:def 13 ex y being Point of (TOP-REAL 3) st hx,y are_antipodals_of p,r,ftake
hy
;
hx,hy are_antipodals_of p,r,f
x,
y are_antipodals_of 0. (TOP-REAL 3),1
by A3;
hence
hx,
hy are_antipodals_of p,
r
by Th55;
BORSUK_7:def 12 ( hx in dom f & hy in dom f & f . hx = f . hy )thus
hx in dom f
by A2, A4, FUNCT_2:5;
( hy in dom f & f . hx = f . hy )thus
hy in dom f
by A2, A5, FUNCT_2:5;
f . hx = f . hythus f . hx =
(f * h) . x
by A4, FUNCT_2:15
.=
f . hy
by A5, A6, FUNCT_2:15
;
verum end; suppose A7:
r is
zero
;
f is with_antipodals take
p
;
BORSUK_7:def 13 ex y being Point of (TOP-REAL 3) st p,y are_antipodals_of p,r,ftake
p
;
p,p are_antipodals_of p,r,freconsider e =
p as
Point of
(Euclid 3) by TOPREAL3:8;
A8: the
carrier of
(Tcircle (p,r)) =
Sphere (
p,
r)
by TOPREALB:9
.=
Sphere (
e,
r)
by TOPREAL9:15
.=
{e}
by A7, TOPREAL6:54
;
thus
p,
p are_antipodals_of p,
r
by A8, TARSKI:def 1, RLTOPSP1:68;
BORSUK_7:def 12 ( p in dom f & p in dom f & f . p = f . p )thus
(
p in dom f &
p in dom f )
by A2, A8, TARSKI:def 1;
f . p = f . pthus
f . p = f . p
;
verum end;