let r be Real; :: thesis: for n being non zero Element of NAT
for p being Point of (TOP-REAL (n + 1)) st r <= 1 & |.p.| >= 1 & |.p.| < 1 + r & p . (n + 1) > 0 & p | n = 0* n holds
ex c being Real ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),c)) st
( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),c) )
let n be non zero Element of NAT ; :: thesis: for p being Point of (TOP-REAL (n + 1)) st r <= 1 & |.p.| >= 1 & |.p.| < 1 + r & p . (n + 1) > 0 & p | n = 0* n holds
ex c being Real ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),c)) st
( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),c) )
set n1 = n + 1;
set TR = TOP-REAL n;
set TR1 = TOP-REAL (n + 1);
set Sp = { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) >= 0 & |.q.| = 1 ) } ;
set Sn = { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) <= 0 & |.q.| = 1 ) } ;
A1: { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) >= 0 & |.q.| = 1 ) } c= the carrier of (TOP-REAL (n + 1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) >= 0 & |.q.| = 1 ) } or x in the carrier of (TOP-REAL (n + 1)) )
assume x in { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) >= 0 & |.q.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL (n + 1))
then ex p being Point of (TOP-REAL (n + 1)) st
( p = x & p . (n + 1) >= 0 & |.p.| = 1 ) ;
hence x in the carrier of (TOP-REAL (n + 1)) ; :: thesis: verum

end;

{ q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) <= 0 & |.q.| = 1 ) } c= the carrier of (TOP-REAL (n + 1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) <= 0 & |.q.| = 1 ) } or x in the carrier of (TOP-REAL (n + 1)) )
assume x in { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) <= 0 & |.q.| = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL (n + 1))
then ex p being Point of (TOP-REAL (n + 1)) st
( p = x & p . (n + 1) <= 0 & |.p.| = 1 ) ;
hence x in the carrier of (TOP-REAL (n + 1)) ; :: thesis: verum

end;

then reconsider Sp = { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) >= 0 & |.q.| = 1 ) } , Sn = { q where q is Point of (TOP-REAL (n + 1)) : ( q . (n + 1) <= 0 & |.q.| = 1 ) } as Subset of (TOP-REAL (n + 1)) by A1;
deffunc H₁( Nat) -> Element of K10(K11( the carrier of (TOP-REAL (n + 1)), the carrier of R^1)) = PROJ ((n + 1),$1);
consider F being FinSequence such that
A2: ( len F = n & ( for k being Nat st k in dom F holds
F . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng F c= Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1) )
assume x in rng F ; :: thesis: x in Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1)
then consider i being object such that
A3: i in dom F and
A4: F . i = x by FUNCT_1:def 3;
reconsider i = i as Nat by A3;
H₁(i) in Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1) by FUNCT_2:8;
hence x in Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1) by A2, A3, A4; :: thesis: verum

end;

then reconsider F = F as FinSequence of Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1) by FINSEQ_1:def 4;
reconsider F = F as Element of n -tuples_on (Funcs ( the carrier of (TOP-REAL (n + 1)), the carrier of R^1)) by A2, FINSEQ_2:92;
set FF = <:F:>;
let p be Point of (TOP-REAL (n + 1)); :: thesis: ( r <= 1 & |.p.| >= 1 & |.p.| < 1 + r & p . (n + 1) > 0 & p | n = 0* n implies ex c being Real ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),c)) st
( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),c) ) )
assume that
A5: r <= 1 and
A6: |.p.| >= 1 and
A7: |.p.| < 1 + r and
A8: p . (n + 1) > 0 and
A9: p | n = 0* n ; :: thesis: ex c being Real ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),c)) st
( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),c) )
set pn1 = p . (n + 1);
A10: 1 + 0 < 1 + ((p . (n + 1)) * (p . (n + 1))) by A8, XREAL_1:6;
rng p c= REAL ;
then A11: p is FinSequence of REAL by FINSEQ_1:def 4;
len p = n + 1 by CARD_1:def 7;
then reconsider P = p as Element of REAL (n + 1) by A11, FINSEQ_2:92;
|.(P | n).| = 0 by A9, EUCLID:7;
then |.(P | n).| ^2 = 0 ;
then |.p.| ^2 = 0 + ((p . (n + 1)) ^2) by REAL_NS1:10;
then A12: ( |.p.| = p . (n + 1) or |.p.| = - (p . (n + 1)) ) by SQUARE_1:40;
then A13: (p . (n + 1)) - 1 < r by A8, A7, XREAL_1:19;
set SP = Sphere ((0. (TOP-REAL (n + 1))),1);
set CL = cl_Ball (p,r);
A15: for q being Point of (TOP-REAL (n + 1)) holds p - q = (- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))

proof

let q be Point of (TOP-REAL (n + 1)); :: thesis: p - q = (- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))
set q1 = (- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))));
A16: len (p - q) = n + 1 by CARD_1:def 7;
A17: len (- q) = n + 1 by CARD_1:def 7;
for i being Nat st 1 <= i & i <= n + 1 holds
(p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n + 1 implies (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i )
assume that
A19: 1 <= i and
A20: i <= n + 1 ; :: thesis: (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i
A21: i in dom (- q) by A19, A20, A17, FINSEQ_3:25;
i in dom (p - q) by A19, A20, A16, FINSEQ_3:25;
then A22: (p - q) . i = (p . i) - (q . i) by VALUED_1:13;

per cases ( i <= n or i = n + 1 ) by A20, NAT_1:8;

suppose A23: i <= n ; :: thesis: (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i

then i < n + 1 by NAT_1:13;
then A24: ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i = (- q) . i by FUNCT_7:32
.= - (q . i) by VALUED_1:8 ;
p . i = (p | (Seg n)) . i by A23, A19, FINSEQ_1:1, FUNCT_1:49;
then p . i = 0 by A9;
hence (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i by A24, A22; :: thesis: verum

end;

suppose i = n + 1 ; :: thesis: (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i

hence (p - q) . i = ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1))))) . i by A21, FUNCT_7:31, A22; :: thesis: verum

end;

end;

end;

hence p - q = (- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1)))) by A16, CARD_1:def 7; :: thesis: verum

end;

set dd = ((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)));
set cc = 1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))));
set c = sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))));
set TD = Tdisk ((0. (TOP-REAL n)),1);
set Tc = Tdisk ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))));
A25: [#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
1 < 1 + r by A6, A7, XXREAL_0:2;
then A26: r > 0 by XREAL_1:32;
then r * r <= 1 * 1 by A5, XREAL_1:66;
then r * r < 1 + ((p . (n + 1)) * (p . (n + 1))) by A10, XXREAL_0:2;
then A27: 0 < (1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r) by XREAL_1:50;
A28: 1 <= n + 1 by NAT_1:11;
A29: for q being Point of (TOP-REAL (n + 1)) holds |.(q - p).| ^2 = ((|.q.| ^2) - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1)))

proof

let q be Point of (TOP-REAL (n + 1)); :: thesis: |.(q - p).| ^2 = ((|.q.| ^2) - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1)))
set pqn = (p . (n + 1)) - (q . (n + 1));
A30: (- q) . (n + 1) = - (q . (n + 1)) by VALUED_1:8;
len (- q) = n + 1 by CARD_1:def 7;
then A31: n + 1 in dom (- q) by A28, FINSEQ_3:25;
|.(q - p).| = |.(- (q - p)).| by EUCLID:10
.= |.(p - q).| by RLVECT_1:33 ;
hence |.(q - p).| ^2 = Sum (sqr (p - q)) by TOPREAL9:5
.= Sum (sqr ((- q) +* ((n + 1),((p . (n + 1)) - (q . (n + 1)))))) by A15
.= ((Sum (sqr (- q))) - (((- q) . (n + 1)) ^2)) + (((p . (n + 1)) - (q . (n + 1))) ^2) by A31, MATRTOP3:3
.= ((|.(- q).| ^2) - (((- q) . (n + 1)) ^2)) + (((p . (n + 1)) - (q . (n + 1))) ^2) by TOPREAL9:5
.= ((|.q.| ^2) - ((- (q . (n + 1))) * (- (q . (n + 1))))) + (((p . (n + 1)) - (q . (n + 1))) ^2) by A30, EUCLID:10
.= ((|.q.| ^2) - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) ;
:: thesis: verum

end;

A32: (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) c= Sp

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) or x in Sp )
assume A33: x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) ; :: thesis: x in Sp
then reconsider x = x as Point of (TOP-REAL (n + 1)) ;
x in cl_Ball (p,r) by A33, XBOOLE_0:def 4;
then A34: |.(x - p).| <= r by TOPREAL9:8;
set xn1 = x . (n + 1);
rng x c= REAL ;
then A35: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n + 1 by CARD_1:def 7;
then reconsider X = x as Element of REAL (n + 1) by A35, FINSEQ_2:92;
x in Sphere ((0. (TOP-REAL (n + 1))),1) by A33, XBOOLE_0:def 4;
then A36: |.x.| = 1 by TOPREAL9:12;
|.(x - p).| ^2 = ((|.x.| ^2) - ((2 * (x . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A29;
then (- ((2 * (x . (n + 1))) * (p . (n + 1)))) + (1 + ((p . (n + 1)) * (p . (n + 1)))) <= r * r by A34, XREAL_1:66, A36;
then - ((2 * (x . (n + 1))) * (p . (n + 1))) <= (r * r) - (1 + ((p . (n + 1)) * (p . (n + 1)))) by XREAL_1:19;
then - ((2 * (x . (n + 1))) * (p . (n + 1))) <= - ((1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r)) ;
then x . (n + 1) >= 0 by XREAL_1:24, A8, A27;
hence x in Sp by A36; :: thesis: verum

end;

A37: <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) c= cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) or y in cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) )
assume y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) ; :: thesis: y in cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))
then consider x being object such that
A38: x in dom <:F:> and
A39: x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) and
A40: <:F:> . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL (n + 1)) by A38;
rng x c= REAL ;
then A41: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n + 1 by CARD_1:def 7;
then reconsider X = x as Element of REAL (n + 1) by A41, FINSEQ_2:92;
x in Sphere ((0. (TOP-REAL (n + 1))),1) by A39, XBOOLE_0:def 4;
then A42: |.x.| = 1 by TOPREAL9:12;
<:F:> . x in rng <:F:> by A38, FUNCT_1:def 3;
then reconsider Y = y as Point of (TOP-REAL n) by A40;
set xn1 = x . (n + 1);
A43: Y - (0. (TOP-REAL n)) = Y by RLVECT_1:13;
x in cl_Ball (p,r) by A39, XBOOLE_0:def 4;
then A44: |.(x - p).| <= r by TOPREAL9:8;
|.(x - p).| ^2 = ((|.x.| ^2) - ((2 * (x . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A29;
then (- ((2 * (x . (n + 1))) * (p . (n + 1)))) + (1 + ((p . (n + 1)) * (p . (n + 1)))) <= r * r by A44, XREAL_1:66, A42;
then - ((2 * (x . (n + 1))) * (p . (n + 1))) <= (r * r) - (1 + ((p . (n + 1)) * (p . (n + 1)))) by XREAL_1:19;
then - ((2 * (x . (n + 1))) * (p . (n + 1))) <= - ((1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r)) ;
then (2 * (p . (n + 1))) * (x . (n + 1)) >= (1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r) by XREAL_1:24;
then x . (n + 1) >= ((1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r)) / (2 * (p . (n + 1))) by A8, XREAL_1:79;
then A45: (x . (n + 1)) * (x . (n + 1)) >= (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) by A8, A27, XREAL_1:66;
|.x.| ^2 = 1 by A42;
then 1 - ((X . (n + 1)) ^2) = ((|.(X | n).| ^2) + ((X . (n + 1)) ^2)) - ((X . (n + 1)) ^2) by REAL_NS1:10
.= |.(X | n).| ^2 ;
then |.(X | n).| ^2 <= 1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))) by A45, XREAL_1:10;
then A46: sqrt (|.(X | n).| ^2) <= sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) by SQUARE_1:26;
<:F:> . x = x | n by A2, Th1;
then |.Y.| <= sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) by SQUARE_1:def 2, A46, A40;
hence y in cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) by A43; :: thesis: verum

end;

[#] ((TOP-REAL (n + 1)) | Sp) = Sp by PRE_TOPC:def 5;
then reconsider SC = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) as Subset of ((TOP-REAL (n + 1)) | Sp) by A32;
A47: ((TOP-REAL (n + 1)) | Sp) | SC = (TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) by A32, PRE_TOPC:7;
A48: Sn = { t where t is Point of (TOP-REAL (n + 1)) : ( t . (n + 1) <= 0 & |.t.| = 1 ) } ;
then A49: <:F:> .: Sp = cl_Ball ((0. (TOP-REAL n)),1) by A2, Th1;
then reconsider FS = <:F:> | Sp as Function of ((TOP-REAL (n + 1)) | Sp),(Tdisk ((0. (TOP-REAL n)),1)) by JORDAN24:12;
Sp = { l where l is Point of (TOP-REAL (n + 1)) : ( l . (n + 1) >= 0 & |.l.| = 1 ) } ;
then reconsider s1 = Sp, s2 = Sn as closed Subset of (TOP-REAL (n + 1)) by Th2, A48;
A50: Ball ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) by TOPREAL9:16;
A51: (p . (n + 1)) - 1 >= 0 by A12, A8, A6, XREAL_1:48;
then A52: ((p . (n + 1)) - 1) * r < r * r by A13, XREAL_1:68;
((p . (n + 1)) - 1) * ((p . (n + 1)) - 1) <= ((p . (n + 1)) - 1) * r by A13, A51, XREAL_1:66;
then (((p . (n + 1)) * (p . (n + 1))) + 1) - (2 * (p . (n + 1))) < r * r by A52, XXREAL_0:2;
then (((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r) < 2 * (p . (n + 1)) by XREAL_1:11;
then A53: ((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))) < 1 by A27, XREAL_1:189;
then (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) < (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * 1 by A8, A27, XREAL_1:68;
then (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) < 1 by A53, XXREAL_0:2;
then A54: 1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))) > 0 by XREAL_1:50;
then A55: 1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))) = (sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))) ^2 by SQUARE_1:def 2;
1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))) < 1 - 0 by A8, A27, XREAL_1:10;
then A56: sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) < sqrt 1 by SQUARE_1:27, A54;
then cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= Ball ((0. (TOP-REAL n)),1) by JORDAN:21;
then A57: cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= cl_Ball ((0. (TOP-REAL n)),1) by A50;
cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) or y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) )
A58: (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) ^2 = (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) ;
assume A59: y in cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) ; :: thesis: y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))
then consider x being object such that
A60: x in dom <:F:> and
A61: x in Sp and
A62: <:F:> . x = y by A57, A49, FUNCT_1:def 6;
y in rng <:F:> by A60, A62, FUNCT_1:def 3;
then reconsider Y = y as Point of (TOP-REAL n) ;
A63: |.Y.| <= sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) by A59, TOPREAL9:11;
consider q being Point of (TOP-REAL (n + 1)) such that
A64: q = x and
A65: q . (n + 1) >= 0 and
A66: |.q.| = 1 by A61;
set qn1 = q . (n + 1);
rng q c= REAL ;
then A67: q is FinSequence of REAL by FINSEQ_1:def 4;
len q = n + 1 by CARD_1:def 7;
then reconsider Q = q as Element of REAL (n + 1) by A67, FINSEQ_2:92;
A68: |.Q.| ^2 = 1 by A66;
then 1 = (|.(Q | n).| ^2) + ((q . (n + 1)) ^2) by REAL_NS1:10
.= (|.Y.| ^2) + ((q . (n + 1)) * (q . (n + 1))) by A2, Th1, A62, A64 ;
then 1 - ((q . (n + 1)) * (q . (n + 1))) <= (sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))) * (sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))) by A63, XREAL_1:66;
then A69: (q . (n + 1)) * (q . (n + 1)) >= (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) by A55, XREAL_1:10;
(q . (n + 1)) ^2 = (q . (n + 1)) * (q . (n + 1)) ;
then ((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))) <= q . (n + 1) by A69, A65, A58, SQUARE_1:47;
then (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (2 * (p . (n + 1))) <= (q . (n + 1)) * (2 * (p . (n + 1))) by A8, XREAL_1:64;
then (((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r) <= (q . (n + 1)) * (2 * (p . (n + 1))) by A8, XCMPLX_1:87;
then A70: (((p . (n + 1)) * (p . (n + 1))) + 1) - ((q . (n + 1)) * (2 * (p . (n + 1)))) <= r * r by XREAL_1:12;
|.(q - p).| ^2 = (1 - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A68, A29;
then |.(q - p).| ^2 <= r ^2 by A70;
then |.(q - p).| <= r by SQUARE_1:47, A26;
then A71: q in cl_Ball (p,r) ;
q - (0. (TOP-REAL (n + 1))) = q by RLVECT_1:13;
then q in Sphere ((0. (TOP-REAL (n + 1))),1) by A66;
then q in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) by A71, XBOOLE_0:def 4;
hence y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r))) by A60, A64, FUNCT_1:def 6, A62; :: thesis: verum

end;

then FS .: SC = cl_Ball ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) by A37, A32, RELAT_1:129;
then A72: (Tdisk ((0. (TOP-REAL n)),1)) | (FS .: SC) = Tdisk ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) by A25, PRE_TOPC:7;
not (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) is empty

proof

A73: (p . (n + 1)) - 1 <= (1 + r) - 1 by A12, A8, A7, XREAL_1:9;
(p . (n + 1)) - 1 >= 0 by A12, A8, A6, XREAL_1:48;
then A74: ((p . (n + 1)) - 1) * ((p . (n + 1)) - 1) <= r * r by A73, XREAL_1:66;
set q = (0* (n + 1)) +* ((n + 1),1);
rng ((0* (n + 1)) +* ((n + 1),1)) c= REAL ;
then W: (0* (n + 1)) +* ((n + 1),1) is FinSequence of REAL by FINSEQ_1:def 4;
len ((0* (n + 1)) +* ((n + 1),1)) = n + 1 by CARD_1:def 7;
then reconsider q = (0* (n + 1)) +* ((n + 1),1) as Point of (TOP-REAL (n + 1)) by W, EUCLID:76;
A75: n + 1 in Seg (n + 1) by FINSEQ_1:4;
A76: |.q.| = |.1.| by FINSEQ_1:4, TOPREALC:13
.= 1 by ABSVALUE:def 1 ;
A77: n + 1 in dom (0* (n + 1)) by A75;
|.q.| ^2 = 1 * 1 by A76;
then |.(q - p).| ^2 = ((1 * 1) - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A29
.= ((1 * 1) - ((2 * 1) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A77, FUNCT_7:31
.= (1 - (p . (n + 1))) * (1 - (p . (n + 1))) ;
then |.(q - p).| ^2 <= r ^2 by A74;
then |.(q - p).| <= r by A26, SQUARE_1:47;
then A78: q in cl_Ball (p,r) ;
q - (0. (TOP-REAL (n + 1))) = q by RLVECT_1:13;
then q in Sphere ((0. (TOP-REAL (n + 1))),1) by A76;
hence not (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)) is empty by A78, XBOOLE_0:def 4; :: thesis: verum

end;

then reconsider H = FS | SC as Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))) by A47, A72, JORDAN24:12;
take sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) ; :: thesis: ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))) st
( sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) )
take H ; :: thesis: ( sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) > 0 & H is being_homeomorphism & H .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) )
for H being Function of ((TOP-REAL (n + 1)) | Sp),(Tdisk ((0. (TOP-REAL n)),1)) st H = <:F:> | Sp holds
H is being_homeomorphism by A2, A48, Th1;
hence ( sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) > 0 & H is being_homeomorphism ) by A47, A72, A54, METRIZTS:2; :: thesis: H .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))
A79: Sphere (p,r) c= cl_Ball (p,r) by TOPREAL9:17;
then (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r)) c= SC by XBOOLE_1:27;
then A80: FS .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) by A32, XBOOLE_1:1, RELAT_1:129;
Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= Ball ((0. (TOP-REAL n)),1) by A56, JORDAN:22;
then A81: Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= cl_Ball ((0. (TOP-REAL n)),1) by A50;
A82: Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) c= <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) or y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) )
A83: (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) ^2 = (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) ;
assume A84: y in Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) ; :: thesis: y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r)))
then consider x being object such that
A85: x in dom <:F:> and
A86: x in Sp and
A87: <:F:> . x = y by A81, A49, FUNCT_1:def 6;
y in rng <:F:> by A85, A87, FUNCT_1:def 3;
then reconsider Y = y as Point of (TOP-REAL n) ;
A88: |.Y.| = sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) by A84, TOPREAL9:12;
consider q being Point of (TOP-REAL (n + 1)) such that
A89: q = x and
A90: q . (n + 1) >= 0 and
A91: |.q.| = 1 by A86;
rng q c= REAL ;
then A92: q is FinSequence of REAL by FINSEQ_1:def 4;
len q = n + 1 by CARD_1:def 7;
then reconsider Q = q as Element of REAL (n + 1) by A92, FINSEQ_2:92;
set qn1 = q . (n + 1);
A93: (q . (n + 1)) ^2 = (q . (n + 1)) * (q . (n + 1)) ;
A94: |.Q.| ^2 = 1 by A91;
then 1 = (|.(Q | n).| ^2) + ((q . (n + 1)) ^2) by REAL_NS1:10
.= (|.Y.| ^2) + ((q . (n + 1)) * (q . (n + 1))) by A2, Th1, A87, A89 ;
then ( ((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))) = q . (n + 1) or ((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))) = - (q . (n + 1)) ) by A88, A55, A93, A83, SQUARE_1:40;
then (((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r) = (q . (n + 1)) * (2 * (p . (n + 1))) by A90, A8, A27, XCMPLX_1:87;
then A95: (((p . (n + 1)) * (p . (n + 1))) + 1) - ((q . (n + 1)) * (2 * (p . (n + 1)))) = r * r ;
|.(q - p).| ^2 = (1 - ((2 * (q . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A94, A29;
then |.(q - p).| ^2 = r ^2 by A95;
then ( |.(q - p).| = r or |.(q - p).| = - r ) by SQUARE_1:40;
then A96: q in Sphere (p,r) by A26;
q - (0. (TOP-REAL (n + 1))) = q by RLVECT_1:13;
then q in Sphere ((0. (TOP-REAL (n + 1))),1) by A91;
then q in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r)) by A96, XBOOLE_0:def 4;
hence y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) by A85, A89, FUNCT_1:def 6, A87; :: thesis: verum

end;

<:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) c= Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) or y in Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) )
assume y in <:F:> .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) ; :: thesis: y in Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))))
then consider x being object such that
A98: x in dom <:F:> and
A99: x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r)) and
A100: <:F:> . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL (n + 1)) by A98;
<:F:> . x in rng <:F:> by A98, FUNCT_1:def 3;
then reconsider Y = y as Point of (TOP-REAL n) by A100;
set xn1 = x . (n + 1);
rng x c= REAL ;
then A101: x is FinSequence of REAL by FINSEQ_1:def 4;
len x = n + 1 by CARD_1:def 7;
then reconsider X = x as Element of REAL (n + 1) by A101, FINSEQ_2:92;
x in Sphere ((0. (TOP-REAL (n + 1))),1) by A99, XBOOLE_0:def 4;
then A102: |.x.| = 1 by TOPREAL9:12;
then |.x.| ^2 = 1 ;
then A103: 1 - ((X . (n + 1)) ^2) = ((|.(X | n).| ^2) + ((X . (n + 1)) ^2)) - ((X . (n + 1)) ^2) by REAL_NS1:10
.= |.(X | n).| ^2 ;
x in Sphere (p,r) by A99, XBOOLE_0:def 4;
then A104: |.(x - p).| = r by TOPREAL9:9;
|.(x - p).| ^2 = ((|.x.| ^2) - ((2 * (x . (n + 1))) * (p . (n + 1)))) + ((p . (n + 1)) * (p . (n + 1))) by A29;
then (2 * (p . (n + 1))) * (x . (n + 1)) = (1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r) by A102, A104;
then x . (n + 1) = ((1 + ((p . (n + 1)) * (p . (n + 1)))) - (r * r)) / (2 * (p . (n + 1))) by A8, XCMPLX_1:89;
then ( |.(X | n).| = sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) or |.(X | n).| = - (sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1))))))) ) by A103, SQUARE_1:def 2;
then A105: |.Y.| = sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))) by A54, A100, A2, Th1;
Y - (0. (TOP-REAL n)) = Y by RLVECT_1:13;
hence y in Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) by A105; :: thesis: verum

end;

hence H .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),(sqrt (1 - ((((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))) * (((((p . (n + 1)) * (p . (n + 1))) + 1) - (r * r)) / (2 * (p . (n + 1)))))))) by A80, A82, A79, XBOOLE_1:27, RELAT_1:129; :: thesis: verum