let a be real number ; :: thesis: for r being non negative real number
for n being non empty Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) holds
HC s,t,o,r = ((1 - a) * s) + (a * t)
let r be non negative real number ; :: thesis: for n being non empty Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) holds
HC s,t,o,r = ((1 - a) * s) + (a * t)
let n be non empty Element of NAT ; :: thesis: for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) holds
HC s,t,o,r = ((1 - a) * s) + (a * t)
let s, t, o be Point of (TOP-REAL n); :: thesis: for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) holds
HC s,t,o,r = ((1 - a) * s) + (a * t)
let S, T, O be Element of REAL n; :: thesis: ( S = s & T = t & O = o & s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) implies HC s,t,o,r = ((1 - a) * s) + (a * t) )
assume that
A1: ( S = s & T = t & O = o ) and
A2: s is Point of (Tdisk o,r) and
A3: t is Point of (Tdisk o,r) and
A4: s <> t ; :: thesis: ( not a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) or HC s,t,o,r = ((1 - a) * s) + (a * t) )
set H = HC s,t,o,r;
set M = |((t - s),(s - o))|;
set A = Sum (sqr (T - S));
set B = 2 * |((t - s),(s - o))|;
set C = (Sum (sqr (S - O))) - (r ^2 );
set l1 = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))));
set l2 = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))));
assume A5: a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) ; :: thesis: HC s,t,o,r = ((1 - a) * s) + (a * t)
A6: HC s,t,o,r in (halfline s,t) /\ (Sphere o,r) by A2, A3, A4, Def3;
then HC s,t,o,r in halfline s,t by XBOOLE_0:def 4;
then consider l being real number such that
A7: HC s,t,o,r = ((1 - l) * s) + (l * t) and
A8: 0 <= l by TOPREAL9:26;
A9: HC s,t,o,r = ((1 * s) - (l * s)) + (l * t) by A7, EUCLID:54
.= (s - (l * s)) + (l * t) by EUCLID:33
.= (s + (l * t)) - (l * s) by JORDAN2C:9
.= s + ((l * t) - (l * s)) by EUCLID:49
.= s + (l * (t - s)) by EUCLID:53 ;
A10: |.(T - S).| <> 0 by A1, A4, EUCLID:19;

A11: now

assume Sum (sqr (T - S)) <= 0 ; :: thesis: contradiction
then Sum (sqr (T - S)) = 0 by RVSUM_1:116;
hence contradiction by A10, EUCLID:def 5, SQUARE_1:82; :: thesis: verum

end;

A12: delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )) = ((2 * |((t - s),(s - o))|) ^2 ) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2 ))) by QUIN_1:def 1
.= 4 * ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))) ;
the carrier of (Tdisk o,r) = cl_Ball o,r by Th3;
then A13: |.(s - o).| <= r by A2, TOPREAL9:8;
A14: |.(S - O).| = sqrt (Sum (sqr (S - O))) by EUCLID:def 5;
A15: |.(T - S).| = sqrt (Sum (sqr (T - S))) by EUCLID:def 5;
Sum (sqr (T - S)) >= 0 by RVSUM_1:116;
then A16: |.(T - S).| ^2 = Sum (sqr (T - S)) by A15, SQUARE_1:def 4;
Sum (sqr (S - O)) >= 0 by RVSUM_1:116;
then A17: |.(S - O).| ^2 = Sum (sqr (S - O)) by A14, SQUARE_1:def 4;
|.(S - O).| <= r by A1, A13, A14, EUCLID:73;
then A18: (sqrt (Sum (sqr (S - O)))) ^2 <= r ^2 by A1, A13, A14, SQUARE_1:77;
then A19: (Sum (sqr (S - O))) - (r ^2 ) <= 0 by A14, A17, XREAL_1:49;
A20: delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )) = ((2 * |((t - s),(s - o))|) ^2 ) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2 ))) by QUIN_1:def 1;
4 * (Sum (sqr (T - S))) > 0 by A11, XREAL_1:131;
then (4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2 )) <= 0 by A19;
then A21: ((2 * |((t - s),(s - o))|) ^2 ) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2 ))) >= 0 ;
l is Real by XREAL_0:def 1;
then A22: |.(l * (t - s)).| ^2 = ((abs l) * |.(t - s).|) ^2 by TOPRNS_1:8
.= ((abs l) ^2 ) * (|.(t - s).| ^2 )
.= (l ^2 ) * (|.(t - s).| ^2 ) by COMPLEX1:161 ;
X: ( s - o = S - O & t - s = T - S ) by A1, EUCLID:73;
HC s,t,o,r in Sphere o,r by A6, XBOOLE_0:def 4;
then r = |.((((1 - l) * s) + (l * t)) - o).| by A7, TOPREAL9:9
.= |.((((1 * s) - (l * s)) + (l * t)) - o).| by EUCLID:54
.= |.(((s - (l * s)) + (l * t)) - o).| by EUCLID:33
.= |.((s - ((l * s) - (l * t))) - o).| by EUCLID:51
.= |.((s - o) - ((l * s) - (l * t))).| by TOPREAL9:1
.= |.((s - o) + (- (l * (s - t)))).| by EUCLID:53
.= |.((s - o) + (l * (- (s - t)))).| by EUCLID:44
.= |.((s - o) + (l * (t - s))).| by EUCLID:48 ;
then Y: r ^2 = ((|.(s - o).| ^2 ) + (2 * |((l * (t - s)),(s - o))|)) + (|.(l * (t - s)).| ^2 ) by EUCLID_2:67
.= ((|.(s - o).| ^2 ) + (2 * (l * |((t - s),(s - o))|))) + (|.(l * (t - s)).| ^2 ) by EUCLID_2:41 ;
then (((Sum (sqr (T - S))) * (l ^2 )) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2 )) = (((Sum (sqr (T - S))) * (l ^2 )) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2 ))
.= (((|.(T - S).| ^2 ) * (l ^2 )) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(S - O).| ^2 ) - (r ^2 )) by A16, A17
.= (((|.(t - s).| ^2 ) * (l ^2 )) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(s - o).| ^2 ) - (r ^2 )) by X
.= 0 by A1, A16, A17, A22, X, Y ;
then A23: Polynom (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )),l = 0 by POLYEQ_1:def 2;
(Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )) <= 0 by A11, A19;
then - 0 <= - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 ))) ;
then 0 + 0 <= (|((t - s),(s - o))| ^2 ) + (- ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))) ;
then A24: ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + ((sqrt 4) * (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 ))))))) / (2 * (Sum (sqr (T - S)))) by A12, SQUARE_1:97
.= (2 * (- (|((t - s),(s - o))| - (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))))) / (2 * (Sum (sqr (T - S)))) by SQUARE_1:85
.= a by A5, XCMPLX_1:92 ;
A25: ( l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) ) by A11, A20, A21, A23, POLYEQ_1:5;

now

let x be real number ; :: thesis: Polynom (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )),x = Quard (Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))),x
thus Polynom (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )),x = (((Sum (sqr (T - S))) * (x ^2 )) + ((2 * |((t - s),(s - o))|) * x)) + ((Sum (sqr (S - O))) - (r ^2 )) by POLYEQ_1:def 2
.= ((Sum (sqr (T - S))) * (x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))))) by A11, A20, A21, QUIN_1:16
.= (Sum (sqr (T - S))) * ((x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))))))
.= Quard (Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))),x by POLYEQ_1:def 3 ; :: thesis: verum

end;

then A26: ((Sum (sqr (S - O))) - (r ^2 )) / (Sum (sqr (T - S))) = (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S))))) by A11, POLYEQ_1:11;
A27: 2 * (Sum (sqr (T - S))) > 0 by A11, XREAL_1:131;

A28: now

set D = sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )));
assume ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) > ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: contradiction
then (- (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) - (2 * |((t - s),(s - o))|) > (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) - (2 * |((t - s),(s - o))|) by A27, XREAL_1:74;
then - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) > sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))) by XREAL_1:11;
then A29: (- (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) > (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) by XREAL_1:8;
0 <= sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))) by A20, A21;
then 0 + 0 <= (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 )))) ;
hence contradiction by A29; :: thesis: verum

end;

per cases ( (Sum (sqr (S - O))) - (r ^2 ) < 0 or ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) or (Sum (sqr (S - O))) - (r ^2 ) = 0 ) by A14, A17, A18, XREAL_1:49;

suppose (Sum (sqr (S - O))) - (r ^2 ) < 0 ; :: thesis: HC s,t,o,r = ((1 - a) * s) + (a * t)

then ((Sum (sqr (S - O))) - (r ^2 )) / (Sum (sqr (T - S))) < 0 by A11, XREAL_1:143;
hence HC s,t,o,r = ((1 - a) * s) + (a * t) by A7, A8, A24, A25, A26, A28; :: thesis: verum

end;

suppose ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: HC s,t,o,r = ((1 - a) * s) + (a * t)

hence HC s,t,o,r = ((1 - a) * s) + (a * t) by A7, A24, A25; :: thesis: verum

end;

suppose A30: (Sum (sqr (S - O))) - (r ^2 ) = 0 ; :: thesis: HC s,t,o,r = ((1 - a) * s) + (a * t)

now

assume A31: l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: contradiction

A32: now

assume l = 0 ; :: thesis: contradiction
then HC s,t,o,r = s + (0. (TOP-REAL n)) by A9, EUCLID:33
.= s by EUCLID:31 ;
hence contradiction by A2, A3, A4, Def3; :: thesis: verum

end;

per cases ( 0 < 2 * |((t - s),(s - o))| or 2 * |((t - s),(s - o))| <= 0 ) ;

suppose A33: 0 < 2 * |((t - s),(s - o))| ; :: thesis: contradiction

then A34: (- 2) * (2 * |((t - s),(s - o))|) < 0 by XREAL_1:134;
((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (2 * |((t - s),(s - o))|)) / (2 * (Sum (sqr (T - S)))) by A20, A30, A33, SQUARE_1:89;
hence contradiction by A8, A27, A31, A34, XREAL_1:143; :: thesis: verum

end;

suppose 2 * |((t - s),(s - o))| <= 0 ; :: thesis: contradiction

then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta (Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2 ))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (- (2 * |((t - s),(s - o))|))) / (2 * (Sum (sqr (T - S)))) by A20, A30, SQUARE_1:90
.= 0 ;
hence contradiction by A31, A32; :: thesis: verum

end;

end;

end;

hence HC s,t,o,r = ((1 - a) * s) + (a * t) by A7, A24, A25; :: thesis: verum

end;

end;