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 )
proof
per cases ( n = 0 or n > 0 ) ;
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 )
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;
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 )
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;
end;
end;
then consider ROT being additive homogeneous rotation Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) such that
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;
per cases ( n = 0 or n > 0 ) ;
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) )
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)*>}
proof
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;
then A43: ((TOP-REAL (n + 1)) | SCL) --> ZZ = zz .--> (0. (TOP-REAL n)) by A11, ZFMISC_1:33;
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
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;
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;
suppose ( z = <*1*> & z = <*(|.((1 / r) * (q - p)).| - (s * r1))*> ) ; :: thesis: contradiction
hence contradiction by FINSEQ_1:76, A23, A9, A25; :: thesis: verum
end;
suppose ( z = <*1*> & z = <*(|.((1 / r) * (q - p)).| + (s * r1))*> ) ; :: thesis: contradiction
hence contradiction by FINSEQ_1:76, A26, A9, A25; :: thesis: verum
end;
suppose ( z = <*(- 1)*> & z = <*(|.((1 / r) * (q - p)).| - (s * r1))*> ) ; :: thesis: contradiction
then - 1 = r1 * (|.(p - q).| - s) by FINSEQ_1:76, A9, A25;
then |.(p - q).| - s < 0 by A5;
then (|.(p - q).| - s) + s < 0 + s by XREAL_1:6;
hence contradiction by A3; :: thesis: verum
end;
suppose ( z = <*(- 1)*> & z = <*(|.((1 / r) * (q - p)).| + (s * r1))*> ) ; :: thesis: contradiction
hence contradiction by FINSEQ_1:76, A26, A9, A25; :: thesis: verum
end;
end;
end;
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;
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
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;
hence HH .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) by A53; :: thesis: verum
reconsider P = p, Q = q as Point of (Euclid (n + 1)) by EUCLID:67;
end;
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) )
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;
A61: now :: thesis: for k being Nat st 1 <= k & k <= n holds
(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;
A68: r1 * r = 1 by A1, A27, XCMPLX_1:106;
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;
end;