let n be Nat; :: thesis: for p, q being Point of (TOP-REAL (n + 1))

for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

N: n in NAT by ORDINAL1:def 12;

set n1 = n + 1;

set TR = TOP-REAL n;

set TR1 = TOP-REAL (n + 1);

let p, q be Point of (TOP-REAL (n + 1)); :: thesis: for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

let r, s be Real; :: thesis: ( s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r implies ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) ) )

assume that

A1: s <= r and

A2: r <= |.(p - q).| and

A3: s < |.(p - q).| and

A4: |.(p - q).| < s + r ; :: thesis: ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

reconsider r1 = 1 / r as Real ;

A5: r > 0 by A1, A4;

then A6: r * r1 = 1 by XCMPLX_1:87;

set A = (Sphere (p,r)) /\ (cl_Ball (q,s));

set TR = TOP-REAL n;

set y = (1 / r) * (q - p);

set T = transl ((- p),(TOP-REAL (n + 1)));

set M = mlt (r1,(TOP-REAL (n + 1)));

A7: 0* (n + 1) = 0. (TOP-REAL (n + 1)) by EUCLID:70;

A8: (- p) + p = 0. (TOP-REAL (n + 1)) by RLVECT_1:5;

A9: |.((1 / r) * (q - p)).| = |.r1.| * |.(q - p).| by EUCLID:11

.= r1 * |.(q - p).| by A5, ABSVALUE:def 1 ;

set Y = (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|);

rng ((0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|)) c= REAL ;

then W: (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) is FinSequence of REAL by FINSEQ_1:def 4;

A10: len ((0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|)) = n + 1 by CARD_1:def 7;

then (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) is Element of REAL (n + 1) by W, FINSEQ_2:92;

then reconsider Y = (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) as Point of (TOP-REAL (n + 1)) by EUCLID:22;

set S = Sphere ((0. (TOP-REAL (n + 1))),1);

set CL = cl_Ball (Y,(s * r1));

A11: [#] ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) by PRE_TOPC:def 5;

A12: |.Y.| = |.|.((1 / r) * (q - p)).|.| by TOPREALC:13, FINSEQ_1:3;

then A13: |.Y.| = |.((1 / r) * (q - p)).| by ABSVALUE:def 1;

ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

ROT is being_homeomorphism and

A14: ROT . ((1 / r) * (q - p)) = Y ;

set h = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))));

A15: |.(ROT . (0. (TOP-REAL (n + 1)))).| = |.(0. (TOP-REAL (n + 1))).| by MATRTOP3:def 4

.= |.(0* (n + 1)).| by EUCLID:70

.= 0 by EUCLID:7 ;

A16: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (Sphere (q,s)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (Sphere (q,s))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (Sphere (((- p) + q),s)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (Sphere (((- p) + q),s))) by RELAT_1:126

.= ROT .: (Sphere ((r1 * (q - p)),(s * r1))) by Th16, A5

.= Sphere (Y,(s * r1)) by A14, Th17 ;

ROT . (0. (TOP-REAL (n + 1))) is Element of REAL (n + 1) by EUCLID:22;

then A17: ROT . (0. (TOP-REAL (n + 1))) = 0. (TOP-REAL (n + 1)) by A15, A7, EUCLID:8;

A18: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (Sphere (p,r)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (Sphere (p,r))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (Sphere (((- p) + p),r)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (Sphere ((0. (TOP-REAL (n + 1))),r))) by A8, RELAT_1:126

.= ROT .: (Sphere ((r1 * (0. (TOP-REAL (n + 1)))),(r * r1))) by Th16, A5

.= ROT .: (Sphere ((r1 * (0. (TOP-REAL (n + 1)))),1)) by A5, XCMPLX_1:87

.= ROT .: (Sphere ((0. (TOP-REAL (n + 1))),1)) by RLVECT_1:10

.= Sphere ((0. (TOP-REAL (n + 1))),1) by Th17, A17 ;

reconsider hA = ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) | ((Sphere (p,r)) /\ (cl_Ball (q,s))) as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),((TOP-REAL (n + 1)) | (((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (cl_Ball (q,s))))) by JORDAN24:12;

ROT * (mlt (r1,(TOP-REAL (n + 1)))) is being_homeomorphism by A5, TOPS_2:57;

then A19: (ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1)))) is being_homeomorphism by TOPS_2:57;

then A20: hA is being_homeomorphism by METRIZTS:2;

reconsider TD = Tdisk ((0. (TOP-REAL n)),1) as non empty TopSpace ;

A21: the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by N, BROUWER:3;

((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (cl_Ball (q,s)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (cl_Ball (q,s))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (cl_Ball (((- p) + q),s)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (cl_Ball (((- p) + q),s))) by RELAT_1:126

.= ROT .: (cl_Ball (((1 / r) * (q - p)),(s * r1))) by Th16, A5

.= cl_Ball (Y,(s * r1)) by A14, Th17 ;

then A22: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (cl_Ball (q,s))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) by A18, A5, FUNCT_1:62;

|.(p - q).| - s < (s + r) - s by A4, XREAL_1:9;

then A23: r1 * (|.(p - q).| - s) < 1 by A6, A5, XREAL_1:68;

A24: dom (0* (n + 1)) = Seg (n + 1) ;

q - p = - (p - q) by RLVECT_1:33;

then A25: |.(p - q).| = |.(q - p).| by EUCLID:10;

|.(p - q).| + s >= r + s by A2, XREAL_1:6;

then |.(p - q).| + s > |.(p - q).| by A4, XXREAL_0:2;

then |.(p - q).| + s > r by A2, XXREAL_0:2;

then A26: r1 * (|.(p - q).| + s) > 1 by A6, A5, XREAL_1:68;

A27: s > 0

for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

N: n in NAT by ORDINAL1:def 12;

set n1 = n + 1;

set TR = TOP-REAL n;

set TR1 = TOP-REAL (n + 1);

let p, q be Point of (TOP-REAL (n + 1)); :: thesis: for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

let r, s be Real; :: thesis: ( s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r implies ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) ) )

assume that

A1: s <= r and

A2: r <= |.(p - q).| and

A3: s < |.(p - q).| and

A4: |.(p - q).| < s + r ; :: thesis: ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

reconsider r1 = 1 / r as Real ;

A5: r > 0 by A1, A4;

then A6: r * r1 = 1 by XCMPLX_1:87;

set A = (Sphere (p,r)) /\ (cl_Ball (q,s));

set TR = TOP-REAL n;

set y = (1 / r) * (q - p);

set T = transl ((- p),(TOP-REAL (n + 1)));

set M = mlt (r1,(TOP-REAL (n + 1)));

A7: 0* (n + 1) = 0. (TOP-REAL (n + 1)) by EUCLID:70;

A8: (- p) + p = 0. (TOP-REAL (n + 1)) by RLVECT_1:5;

A9: |.((1 / r) * (q - p)).| = |.r1.| * |.(q - p).| by EUCLID:11

.= r1 * |.(q - p).| by A5, ABSVALUE:def 1 ;

set Y = (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|);

rng ((0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|)) c= REAL ;

then W: (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) is FinSequence of REAL by FINSEQ_1:def 4;

A10: len ((0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|)) = n + 1 by CARD_1:def 7;

then (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) is Element of REAL (n + 1) by W, FINSEQ_2:92;

then reconsider Y = (0* (n + 1)) +* ((n + 1),|.((1 / r) * (q - p)).|) as Point of (TOP-REAL (n + 1)) by EUCLID:22;

set S = Sphere ((0. (TOP-REAL (n + 1))),1);

set CL = cl_Ball (Y,(s * r1));

A11: [#] ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) by PRE_TOPC:def 5;

A12: |.Y.| = |.|.((1 / r) * (q - p)).|.| by TOPREALC:13, FINSEQ_1:3;

then A13: |.Y.| = |.((1 / r) * (q - p)).| by ABSVALUE:def 1;

ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

proof
end;

then consider ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) such that per cases
( n = 0 or n > 0 )
;

end;

suppose
n = 0
; :: thesis: ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

then
ex ROT being additive homogeneous Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is rotation & ROT . ((1 / r) * (q - p)) = Y & ( AutMt ROT = AxialSymmetry ((n + 1),(n + 1)) or AutMt ROT = 1. (F_Real,(n + 1)) ) ) by A13, MATRTOP3:40;

hence ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y ) ; :: thesis: verum

end;( ROT is rotation & ROT . ((1 / r) * (q - p)) = Y & ( AutMt ROT = AxialSymmetry ((n + 1),(n + 1)) or AutMt ROT = 1. (F_Real,(n + 1)) ) ) by A13, MATRTOP3:40;

hence ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y ) ; :: thesis: verum

suppose
n > 0
; :: thesis: ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y )

then
n + 1 <> 1
;

then ex ROT being additive homogeneous Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is base_rotation & ROT . ((1 / r) * (q - p)) = Y ) by A13, MATRTOP3:41;

hence ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y ) ; :: thesis: verum

end;then ex ROT being additive homogeneous Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is base_rotation & ROT . ((1 / r) * (q - p)) = Y ) by A13, MATRTOP3:41;

hence ex ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st

( ROT is being_homeomorphism & ROT . ((1 / r) * (q - p)) = Y ) ; :: thesis: verum

ROT is being_homeomorphism and

A14: ROT . ((1 / r) * (q - p)) = Y ;

set h = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))));

A15: |.(ROT . (0. (TOP-REAL (n + 1)))).| = |.(0. (TOP-REAL (n + 1))).| by MATRTOP3:def 4

.= |.(0* (n + 1)).| by EUCLID:70

.= 0 by EUCLID:7 ;

A16: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (Sphere (q,s)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (Sphere (q,s))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (Sphere (((- p) + q),s)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (Sphere (((- p) + q),s))) by RELAT_1:126

.= ROT .: (Sphere ((r1 * (q - p)),(s * r1))) by Th16, A5

.= Sphere (Y,(s * r1)) by A14, Th17 ;

ROT . (0. (TOP-REAL (n + 1))) is Element of REAL (n + 1) by EUCLID:22;

then A17: ROT . (0. (TOP-REAL (n + 1))) = 0. (TOP-REAL (n + 1)) by A15, A7, EUCLID:8;

A18: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (Sphere (p,r)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (Sphere (p,r))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (Sphere (((- p) + p),r)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (Sphere ((0. (TOP-REAL (n + 1))),r))) by A8, RELAT_1:126

.= ROT .: (Sphere ((r1 * (0. (TOP-REAL (n + 1)))),(r * r1))) by Th16, A5

.= ROT .: (Sphere ((r1 * (0. (TOP-REAL (n + 1)))),1)) by A5, XCMPLX_1:87

.= ROT .: (Sphere ((0. (TOP-REAL (n + 1))),1)) by RLVECT_1:10

.= Sphere ((0. (TOP-REAL (n + 1))),1) by Th17, A17 ;

reconsider hA = ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) | ((Sphere (p,r)) /\ (cl_Ball (q,s))) as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),((TOP-REAL (n + 1)) | (((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (cl_Ball (q,s))))) by JORDAN24:12;

ROT * (mlt (r1,(TOP-REAL (n + 1)))) is being_homeomorphism by A5, TOPS_2:57;

then A19: (ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1)))) is being_homeomorphism by TOPS_2:57;

then A20: hA is being_homeomorphism by METRIZTS:2;

reconsider TD = Tdisk ((0. (TOP-REAL n)),1) as non empty TopSpace ;

A21: the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by N, BROUWER:3;

((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: (cl_Ball (q,s)) = (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: ((transl ((- p),(TOP-REAL (n + 1)))) .: (cl_Ball (q,s))) by RELAT_1:126

.= (ROT * (mlt (r1,(TOP-REAL (n + 1))))) .: (cl_Ball (((- p) + q),s)) by Th15

.= ROT .: ((mlt (r1,(TOP-REAL (n + 1)))) .: (cl_Ball (((- p) + q),s))) by RELAT_1:126

.= ROT .: (cl_Ball (((1 / r) * (q - p)),(s * r1))) by Th16, A5

.= cl_Ball (Y,(s * r1)) by A14, Th17 ;

then A22: ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (cl_Ball (q,s))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) by A18, A5, FUNCT_1:62;

|.(p - q).| - s < (s + r) - s by A4, XREAL_1:9;

then A23: r1 * (|.(p - q).| - s) < 1 by A6, A5, XREAL_1:68;

A24: dom (0* (n + 1)) = Seg (n + 1) ;

q - p = - (p - q) by RLVECT_1:33;

then A25: |.(p - q).| = |.(q - p).| by EUCLID:10;

|.(p - q).| + s >= r + s by A2, XREAL_1:6;

then |.(p - q).| + s > |.(p - q).| by A4, XXREAL_0:2;

then |.(p - q).| + s > r by A2, XXREAL_0:2;

then A26: r1 * (|.(p - q).| + s) > 1 by A6, A5, XREAL_1:68;

A27: s > 0

proof

assume
s <= 0
; :: thesis: contradiction

then s + r <= r + 0 by XREAL_1:6;

hence contradiction by A4, XXREAL_0:2, A2; :: thesis: verum

end;then s + r <= r + 0 by XREAL_1:6;

hence contradiction by A4, XXREAL_0:2, A2; :: thesis: verum

per cases
( n = 0 or n > 0 )
;

end;

suppose A28:
n = 0
; :: thesis: ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

set E = Euclid (n + 1);

reconsider YY = Y as Point of (Euclid (n + 1)) by EUCLID:67;

Y . 1 = |.((1 / r) * (q - p)).| by A24, FINSEQ_1:3, A28, FUNCT_7:31;

then A29: YY = <*|.((1 / r) * (q - p)).|*> by CARD_1:def 7, A28, FINSEQ_1:40;

then A30: cl_Ball (YY,(s * r1)) = { <*w*> where w is Real : ( |.((1 / r) * (q - p)).| - (s * r1) <= w & w <= |.((1 / r) * (q - p)).| + (s * r1) ) } by A28, TOPDIM_2:17;

A31: [#] (TOP-REAL n) = {(0. (TOP-REAL n))} by A28, EUCLID:22, EUCLID:77;

then reconsider ZZ = 0. (TOP-REAL n) as Point of TD by A21, ZFMISC_1:33;

A32: [#] (Tdisk ((0. (TOP-REAL n)),1)) = {(0. (TOP-REAL n))} by A21, A31, ZFMISC_1:33;

reconsider z = 0 , yy = |.((1 / r) * (q - p)).| as Real ;

0. (TOP-REAL (n + 1)) = <*z*> by A7, A28, FINSEQ_2:59;

then A33: Fr (Ball ((0. (TOP-REAL (n + 1))),1)) = {<*(z - 1)*>,<*(z + 1)*>} by A28, TOPDIM_2:18;

A34: Fr (Ball ((0. (TOP-REAL (n + 1))),1)) = Sphere ((0. (TOP-REAL (n + 1))),1) by JORDAN:24;

then A35: <*(z + 1)*> in Sphere ((0. (TOP-REAL (n + 1))),1) by A33, TARSKI:def 2;

A36: cl_Ball (YY,(s * r1)) = cl_Ball (Y,(s * r1)) by TOPREAL9:14;

then A37: <*(z + 1)*> in cl_Ball (Y,(s * r1)) by A23, A9, A25, A26, A30;

then A38: not (Sphere (p,r)) /\ (cl_Ball (q,s)) is empty by A22, A35, XBOOLE_0:def 4;

reconsider SCL = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) as non empty Subset of (TOP-REAL (n + 1)) by A35, A37, XBOOLE_0:def 4;

reconsider zz = <*1*> as Point of ((TOP-REAL (n + 1)) | SCL) by A35, A37, XBOOLE_0:def 4, A11;

set h1 = ((TOP-REAL (n + 1)) | SCL) --> ZZ;

set h2 = TD --> zz;

(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) c= {<*(z + 1)*>}

then rng (((TOP-REAL (n + 1)) | SCL) --> ZZ) = {(0. (TOP-REAL n))} by FUNCOP_1:88;

then ((TOP-REAL (n + 1)) | SCL) --> ZZ is onto by A32, FUNCT_2:def 3;

then A44: (((TOP-REAL (n + 1)) | SCL) --> ZZ) " = (zz .--> (0. (TOP-REAL n))) " by A43, TOPS_2:def 4;

reconsider HA = hA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),((TOP-REAL (n + 1)) | SCL) by A22;

reconsider HH = (((TOP-REAL (n + 1)) | SCL) --> ZZ) * HA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) ;

take HH ; :: thesis: ( HH is being_homeomorphism & HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

A45: dom (((TOP-REAL (n + 1)) | SCL) --> ZZ) = [#] ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))) ;

A46: HA is being_homeomorphism by A19, METRIZTS:2, A22;

TD --> zz = (0. (TOP-REAL n)) .--> zz by A21, A31, ZFMISC_1:33;

then A47: (((TOP-REAL (n + 1)) | SCL) --> ZZ) " is continuous by NECKLACE:9, A44;

rng (((TOP-REAL (n + 1)) | SCL) --> ZZ) = [#] (Tdisk ((0. (TOP-REAL n)),1)) by ZFMISC_1:33, A32;

then ((TOP-REAL (n + 1)) | SCL) --> ZZ is being_homeomorphism by A45, A43, A47, TOPS_2:def 5;

hence HH is being_homeomorphism by A38, TOPS_2:57, A46; :: thesis: HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1)

A48: Fr (Ball (Y,(s * r1))) = Sphere (Y,(s * r1)) by A1, A27, JORDAN:24;

A49: Fr (Ball (Y,(s * r1))) = {<*(|.((1 / r) * (q - p)).| - (s * r1))*>,<*(|.((1 / r) * (q - p)).| + (s * r1))*>} by A1, A27, A29, A28, TOPDIM_2:18;

(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(s * r1))) = {}

then HA .: ((Sphere (p,r)) /\ (Sphere (q,s))) = {} by XBOOLE_1:3, RELAT_1:128;

then A53: HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = (((TOP-REAL (n + 1)) | SCL) --> ZZ) .: {} by RELAT_1:126

.= {} ;

Sphere ((0. (TOP-REAL n)),1) = {}

reconsider P = p, Q = q as Point of (Euclid (n + 1)) by EUCLID:67;

end;reconsider YY = Y as Point of (Euclid (n + 1)) by EUCLID:67;

Y . 1 = |.((1 / r) * (q - p)).| by A24, FINSEQ_1:3, A28, FUNCT_7:31;

then A29: YY = <*|.((1 / r) * (q - p)).|*> by CARD_1:def 7, A28, FINSEQ_1:40;

then A30: cl_Ball (YY,(s * r1)) = { <*w*> where w is Real : ( |.((1 / r) * (q - p)).| - (s * r1) <= w & w <= |.((1 / r) * (q - p)).| + (s * r1) ) } by A28, TOPDIM_2:17;

A31: [#] (TOP-REAL n) = {(0. (TOP-REAL n))} by A28, EUCLID:22, EUCLID:77;

then reconsider ZZ = 0. (TOP-REAL n) as Point of TD by A21, ZFMISC_1:33;

A32: [#] (Tdisk ((0. (TOP-REAL n)),1)) = {(0. (TOP-REAL n))} by A21, A31, ZFMISC_1:33;

reconsider z = 0 , yy = |.((1 / r) * (q - p)).| as Real ;

0. (TOP-REAL (n + 1)) = <*z*> by A7, A28, FINSEQ_2:59;

then A33: Fr (Ball ((0. (TOP-REAL (n + 1))),1)) = {<*(z - 1)*>,<*(z + 1)*>} by A28, TOPDIM_2:18;

A34: Fr (Ball ((0. (TOP-REAL (n + 1))),1)) = Sphere ((0. (TOP-REAL (n + 1))),1) by JORDAN:24;

then A35: <*(z + 1)*> in Sphere ((0. (TOP-REAL (n + 1))),1) by A33, TARSKI:def 2;

A36: cl_Ball (YY,(s * r1)) = cl_Ball (Y,(s * r1)) by TOPREAL9:14;

then A37: <*(z + 1)*> in cl_Ball (Y,(s * r1)) by A23, A9, A25, A26, A30;

then A38: not (Sphere (p,r)) /\ (cl_Ball (q,s)) is empty by A22, A35, XBOOLE_0:def 4;

reconsider SCL = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) as non empty Subset of (TOP-REAL (n + 1)) by A35, A37, XBOOLE_0:def 4;

reconsider zz = <*1*> as Point of ((TOP-REAL (n + 1)) | SCL) by A35, A37, XBOOLE_0:def 4, A11;

set h1 = ((TOP-REAL (n + 1)) | SCL) --> ZZ;

set h2 = TD --> zz;

(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) c= {<*(z + 1)*>}

proof

then A43:
((TOP-REAL (n + 1)) | SCL) --> ZZ = zz .--> (0. (TOP-REAL n))
by A11, ZFMISC_1:33;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) or v in {<*(z + 1)*>} )

assume A39: v in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) ; :: thesis: v in {<*(z + 1)*>}

then v in Sphere ((0. (TOP-REAL (n + 1))),1) by XBOOLE_0:def 4;

then A40: ( v = <*(z + 1)*> or v = <*(z - 1)*> ) by A34, A33, TARSKI:def 2;

assume A41: not v in {<*(z + 1)*>} ; :: thesis: contradiction

v in cl_Ball (Y,(s * r1)) by A39, XBOOLE_0:def 4;

then ex w being Real st

( <*(z - 1)*> = <*w*> & |.((1 / r) * (q - p)).| - (s * r1) <= w & w <= |.((1 / r) * (q - p)).| + (s * r1) ) by A41, A40, TARSKI:def 1, A30, A36;

then r1 * (|.(p - q).| - s) <= - (r1 * r) by FINSEQ_1:76, A9, A25, A6;

then r1 * (|.(p - q).| - s) <= r1 * (- r) ;

then A42: r <= - (|.(p - q).| - s) by A5, XREAL_1:68, XREAL_1:25;

s - |.(p - q).| < |.(p - q).| - |.(p - q).| by A3, XREAL_1:14;

hence contradiction by A42, A5; :: thesis: verum

end;assume A39: v in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))) ; :: thesis: v in {<*(z + 1)*>}

then v in Sphere ((0. (TOP-REAL (n + 1))),1) by XBOOLE_0:def 4;

then A40: ( v = <*(z + 1)*> or v = <*(z - 1)*> ) by A34, A33, TARSKI:def 2;

assume A41: not v in {<*(z + 1)*>} ; :: thesis: contradiction

v in cl_Ball (Y,(s * r1)) by A39, XBOOLE_0:def 4;

then ex w being Real st

( <*(z - 1)*> = <*w*> & |.((1 / r) * (q - p)).| - (s * r1) <= w & w <= |.((1 / r) * (q - p)).| + (s * r1) ) by A41, A40, TARSKI:def 1, A30, A36;

then r1 * (|.(p - q).| - s) <= - (r1 * r) by FINSEQ_1:76, A9, A25, A6;

then r1 * (|.(p - q).| - s) <= r1 * (- r) ;

then A42: r <= - (|.(p - q).| - s) by A5, XREAL_1:68, XREAL_1:25;

s - |.(p - q).| < |.(p - q).| - |.(p - q).| by A3, XREAL_1:14;

hence contradiction by A42, A5; :: thesis: verum

then rng (((TOP-REAL (n + 1)) | SCL) --> ZZ) = {(0. (TOP-REAL n))} by FUNCOP_1:88;

then ((TOP-REAL (n + 1)) | SCL) --> ZZ is onto by A32, FUNCT_2:def 3;

then A44: (((TOP-REAL (n + 1)) | SCL) --> ZZ) " = (zz .--> (0. (TOP-REAL n))) " by A43, TOPS_2:def 4;

reconsider HA = hA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),((TOP-REAL (n + 1)) | SCL) by A22;

reconsider HH = (((TOP-REAL (n + 1)) | SCL) --> ZZ) * HA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) ;

take HH ; :: thesis: ( HH is being_homeomorphism & HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

A45: dom (((TOP-REAL (n + 1)) | SCL) --> ZZ) = [#] ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))) ;

A46: HA is being_homeomorphism by A19, METRIZTS:2, A22;

TD --> zz = (0. (TOP-REAL n)) .--> zz by A21, A31, ZFMISC_1:33;

then A47: (((TOP-REAL (n + 1)) | SCL) --> ZZ) " is continuous by NECKLACE:9, A44;

rng (((TOP-REAL (n + 1)) | SCL) --> ZZ) = [#] (Tdisk ((0. (TOP-REAL n)),1)) by ZFMISC_1:33, A32;

then ((TOP-REAL (n + 1)) | SCL) --> ZZ is being_homeomorphism by A45, A43, A47, TOPS_2:def 5;

hence HH is being_homeomorphism by A38, TOPS_2:57, A46; :: thesis: HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1)

A48: Fr (Ball (Y,(s * r1))) = Sphere (Y,(s * r1)) by A1, A27, JORDAN:24;

A49: Fr (Ball (Y,(s * r1))) = {<*(|.((1 / r) * (q - p)).| - (s * r1))*>,<*(|.((1 / r) * (q - p)).| + (s * r1))*>} by A1, A27, A29, A28, TOPDIM_2:18;

(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(s * r1))) = {}

proof

then
((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (Sphere (q,s))) = {}
by A18, A16, FUNCT_1:62, A5;
assume
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(s * r1))) <> {}
; :: thesis: contradiction

then consider z being object such that

A50: z in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(s * r1))) by XBOOLE_0:def 1;

A51: z in Sphere (Y,(s * r1)) by A50, XBOOLE_0:def 4;

A52: z in Sphere ((0. (TOP-REAL (n + 1))),1) by A50, XBOOLE_0:def 4;

end;then consider z being object such that

A50: z in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(s * r1))) by XBOOLE_0:def 1;

A51: z in Sphere (Y,(s * r1)) by A50, XBOOLE_0:def 4;

A52: z in Sphere ((0. (TOP-REAL (n + 1))),1) by A50, XBOOLE_0:def 4;

per cases
( ( z = <*1*> & z = <*(|.((1 / r) * (q - p)).| - (s * r1))*> ) or ( z = <*1*> & z = <*(|.((1 / r) * (q - p)).| + (s * r1))*> ) or ( z = <*(- 1)*> & z = <*(|.((1 / r) * (q - p)).| - (s * r1))*> ) or ( z = <*(- 1)*> & z = <*(|.((1 / r) * (q - p)).| + (s * r1))*> ) )
by A52, A34, A33, TARSKI:def 2, A51, A48, A49;

end;

then HA .: ((Sphere (p,r)) /\ (Sphere (q,s))) = {} by XBOOLE_1:3, RELAT_1:128;

then A53: HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = (((TOP-REAL (n + 1)) | SCL) --> ZZ) .: {} by RELAT_1:126

.= {} ;

Sphere ((0. (TOP-REAL n)),1) = {}

proof

hence
HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1)
by A53; :: thesis: verum
assume
Sphere ((0. (TOP-REAL n)),1) <> {}
; :: thesis: contradiction

then consider w being object such that

A54: w in Sphere ((0. (TOP-REAL n)),1) by XBOOLE_0:def 1;

w = 0. (TOP-REAL n) by A54, A28, EUCLID:77;

then A55: |.(0. (TOP-REAL n)).| = 1 by A54, TOPREAL9:12;

0. (TOP-REAL n) = 0* n by EUCLID:70;

hence contradiction by A55, EUCLID:7; :: thesis: verum

end;then consider w being object such that

A54: w in Sphere ((0. (TOP-REAL n)),1) by XBOOLE_0:def 1;

w = 0. (TOP-REAL n) by A54, A28, EUCLID:77;

then A55: |.(0. (TOP-REAL n)).| = 1 by A54, TOPREAL9:12;

0. (TOP-REAL n) = 0* n by EUCLID:70;

hence contradiction by A55, EUCLID:7; :: thesis: verum

reconsider P = p, Q = q as Point of (Euclid (n + 1)) by EUCLID:67;

suppose A56:
n > 0
; :: thesis: ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

A57:
len (0* n) = n
by CARD_1:def 7;

r1 * |.(p - q).| < r1 * (s + r) by A27, A1, A4, XREAL_1:68;

then |.Y.| < (r1 * r) + (r1 * s) by A9, A25, A12, ABSVALUE:def 1;

then A58: |.Y.| < 1 + (r1 * s) by A1, A27, XCMPLX_1:106;

A59: n < n + 1 by NAT_1:13;

then A60: len (Y | n) = n by A10, FINSEQ_1:59;

then A69: r1 * s <= 1 by A1, XREAL_1:64, A27;

|.((1 / r) * (q - p)).| >= 1 by XREAL_1:64, A27, A1, A2, A9, A25, A68;

then A70: |.Y.| >= 1 by A12, ABSVALUE:def 1;

Y . (n + 1) > 0 by A2, A5, A9, A25, FINSEQ_1:3, FUNCT_7:31, A24;

then consider c being Real, H being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))),(Tdisk ((0. (TOP-REAL n)),c)) such that

A71: c > 0 and

A72: H is being_homeomorphism and

A73: H .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(r1 * s)))) = Sphere ((0. (TOP-REAL n)),c) by A56, Lm4, A69, A70, A58, A61, FINSEQ_1:14, A57, A60;

rng H = [#] (Tdisk ((0. (TOP-REAL n)),c)) by A72, TOPS_2:def 5;

then A74: not (Sphere (p,r)) /\ (cl_Ball (q,s)) is empty by A71, A22;

then reconsider HH = H * hA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),c)) by A22;

A75: HH is being_homeomorphism by A71, A72, A74, A20, A22, TOPS_2:57;

reconsider c1 = 1 / c as Real ;

set MM = mlt (c1,(TOP-REAL n));

A76: c1 * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10;

A77: c1 * c = 1 by A71, XCMPLX_1:106;

then A78: (mlt (c1,(TOP-REAL n))) .: (cl_Ball ((0. (TOP-REAL n)),c)) = cl_Ball ((0. (TOP-REAL n)),1) by A71, A76, Th16;

then reconsider MM1 = (mlt (c1,(TOP-REAL n))) | (cl_Ball ((0. (TOP-REAL n)),c)) as Function of (Tdisk ((0. (TOP-REAL n)),c)),(Tdisk ((0. (TOP-REAL n)),1)) by JORDAN24:12;

reconsider MH = MM1 * HH as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) by A71;

take MH ; :: thesis: ( MH is being_homeomorphism & MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

MM1 is being_homeomorphism by METRIZTS:2, A71, A78;

hence MH is being_homeomorphism by A75, A71, A74, TOPS_2:57; :: thesis: MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1)

Sphere (q,s) c= cl_Ball (q,s) by TOPREAL9:17;

then hA .: ((Sphere (p,r)) /\ (Sphere (q,s))) = ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (Sphere (q,s))) by XBOOLE_1:27, RELAT_1:129;

then HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = H .: (((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (Sphere (q,s)))) by RELAT_1:126

.= Sphere ((0. (TOP-REAL n)),c) by A73, A18, A16, FUNCT_1:62, A5 ;

hence MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = MM1 .: (Sphere ((0. (TOP-REAL n)),c)) by RELAT_1:126

.= (mlt (c1,(TOP-REAL n))) .: (Sphere ((0. (TOP-REAL n)),c)) by TOPREAL9:17, RELAT_1:129

.= Sphere ((0. (TOP-REAL n)),1) by Th16, A71, A76, A77 ;

:: thesis: verum

end;r1 * |.(p - q).| < r1 * (s + r) by A27, A1, A4, XREAL_1:68;

then |.Y.| < (r1 * r) + (r1 * s) by A9, A25, A12, ABSVALUE:def 1;

then A58: |.Y.| < 1 + (r1 * s) by A1, A27, XCMPLX_1:106;

A59: n < n + 1 by NAT_1:13;

then A60: len (Y | n) = n by A10, FINSEQ_1:59;

A61: now :: thesis: for k being Nat st 1 <= k & k <= n holds

(Y | n) . k = (0* n) . k

A68:
r1 * r = 1
by A1, A27, XCMPLX_1:106;(Y | n) . k = (0* n) . k

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Y | n) . k = (0* n) . k )

assume that

A64: 1 <= k and

A65: k <= n ; :: thesis: (Y | n) . k = (0* n) . k

A66: Y . k = (0* (n + 1)) . k by A65, A59, FUNCT_7:32;

(Y | n) . k = Y . k by A64, A65, FINSEQ_1:1, FUNCT_1:49;

hence (Y | n) . k = (0* n) . k by A66; :: thesis: verum

end;assume that

A64: 1 <= k and

A65: k <= n ; :: thesis: (Y | n) . k = (0* n) . k

A66: Y . k = (0* (n + 1)) . k by A65, A59, FUNCT_7:32;

(Y | n) . k = Y . k by A64, A65, FINSEQ_1:1, FUNCT_1:49;

hence (Y | n) . k = (0* n) . k by A66; :: thesis: verum

then A69: r1 * s <= 1 by A1, XREAL_1:64, A27;

|.((1 / r) * (q - p)).| >= 1 by XREAL_1:64, A27, A1, A2, A9, A25, A68;

then A70: |.Y.| >= 1 by A12, ABSVALUE:def 1;

Y . (n + 1) > 0 by A2, A5, A9, A25, FINSEQ_1:3, FUNCT_7:31, A24;

then consider c being Real, H being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (Y,(s * r1))))),(Tdisk ((0. (TOP-REAL n)),c)) such that

A71: c > 0 and

A72: H is being_homeomorphism and

A73: H .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (Y,(r1 * s)))) = Sphere ((0. (TOP-REAL n)),c) by A56, Lm4, A69, A70, A58, A61, FINSEQ_1:14, A57, A60;

rng H = [#] (Tdisk ((0. (TOP-REAL n)),c)) by A72, TOPS_2:def 5;

then A74: not (Sphere (p,r)) /\ (cl_Ball (q,s)) is empty by A71, A22;

then reconsider HH = H * hA as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),c)) by A22;

A75: HH is being_homeomorphism by A71, A72, A74, A20, A22, TOPS_2:57;

reconsider c1 = 1 / c as Real ;

set MM = mlt (c1,(TOP-REAL n));

A76: c1 * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10;

A77: c1 * c = 1 by A71, XCMPLX_1:106;

then A78: (mlt (c1,(TOP-REAL n))) .: (cl_Ball ((0. (TOP-REAL n)),c)) = cl_Ball ((0. (TOP-REAL n)),1) by A71, A76, Th16;

then reconsider MM1 = (mlt (c1,(TOP-REAL n))) | (cl_Ball ((0. (TOP-REAL n)),c)) as Function of (Tdisk ((0. (TOP-REAL n)),c)),(Tdisk ((0. (TOP-REAL n)),1)) by JORDAN24:12;

reconsider MH = MM1 * HH as Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) by A71;

take MH ; :: thesis: ( MH is being_homeomorphism & MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

MM1 is being_homeomorphism by METRIZTS:2, A71, A78;

hence MH is being_homeomorphism by A75, A71, A74, TOPS_2:57; :: thesis: MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1)

Sphere (q,s) c= cl_Ball (q,s) by TOPREAL9:17;

then hA .: ((Sphere (p,r)) /\ (Sphere (q,s))) = ((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (Sphere (q,s))) by XBOOLE_1:27, RELAT_1:129;

then HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = H .: (((ROT * (mlt (r1,(TOP-REAL (n + 1))))) * (transl ((- p),(TOP-REAL (n + 1))))) .: ((Sphere (p,r)) /\ (Sphere (q,s)))) by RELAT_1:126

.= Sphere ((0. (TOP-REAL n)),c) by A73, A18, A16, FUNCT_1:62, A5 ;

hence MH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = MM1 .: (Sphere ((0. (TOP-REAL n)),c)) by RELAT_1:126

.= (mlt (c1,(TOP-REAL n))) .: (Sphere ((0. (TOP-REAL n)),c)) by TOPREAL9:17, RELAT_1:129

.= Sphere ((0. (TOP-REAL n)),1) by Th16, A71, A76, A77 ;

:: thesis: verum