let T be non empty TopSpace; :: thesis:
assume A1: T is T_1 ; :: thesis:
set cT = the carrier of T;
set Geo = (1 / 2) GeoSeq ;
let s be Real; :: thesis:
let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; :: thesis:
assume that
A2: for n being Nat ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) and
A3: for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being Nat st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ; :: thesis:
deffunc H₁( Element of the carrier of T, Element of the carrier of T) -> Element of REAL = In ((Sum (((1 / 2) GeoSeq) (#) (FS2 # [$1,$2]))),REAL);
consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A4: for p, q being Point of T holds pmet . (p,q) = H₁(p,q) from BINOP_1:sch 4();
A5: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq))

proof

let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis:
consider p, q being object such that
A6: ( p in the carrier of T & q in the carrier of T ) and
A7: pq = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Element of the carrier of T by A6;
pmet . pq = pmet . (p,q) by A7
.= H₁(p,q) by A4 ;
hence pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) by A7; :: thesis:

end;

A8: for pq being Element of [: the carrier of T, the carrier of T:]
for n being Nat holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )

proof

let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis:
let n be Nat; :: thesis:
consider x, y being object such that
A9: ( x in the carrier of T & y in the carrier of T ) and
A10: [x,y] = pq by ZFMISC_1:def 2;
reconsider x = x, y = y as Point of T by A9;
A11: (((1 / 2) GeoSeq) . n) * s = (s (#) ((1 / 2) GeoSeq)) . n by SEQ_1:9;
(1 / 2) |^ n > 0 by NEWTON:83;
then A12: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def 1;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A13: FS2 . n = pmet1 and
A14: pmet1 is_a_pseudometric_of the carrier of T and
A15: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
A16: 0 <= pmet1 . (x,y) by A14, NAGATA_1:29;
A17: pmet1 . pq = (FS2 # pq) . n by A13, SEQFUNC:def 10;
then (((1 / 2) GeoSeq) . n) * ((FS2 # pq) . n) <= (((1 / 2) GeoSeq) . n) * s by A15, A12, XREAL_1:64;
hence ( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) by A10, A16, A12, A17, A11, SEQ_1:8; :: thesis:

end;

A18: for p, q being Point of T st pmet . (p,q) = 0 holds
p = q

proof

let p, q be Point of T; :: thesis:
assume that
A19: pmet . (p,q) = 0 and
A20: p <> q ; :: thesis:
set Q = {q};
A21: not p in {q} by A20, TARSKI:def 1;
set pq = [p,q];
A22: Sum (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) = 0 by A5, A19;
A23: for n being Nat holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n & (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) by A8;
{q} is closed by A1, URYSOHN1:19;
then consider n being Nat such that
A24: for pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet1 holds
(lower_bound (pmet1,{q})) . p > 0 by A3, A21;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A25: FS2 . n = pmet1 and
A26: pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
(lower_bound (pmet1,{q})) . p > 0 by A24, A25;
then A27: lower_bound ((dist (pmet1,p)) .: {q}) > 0 by Def3;
1 / 2 < 1 ;
then |.(1 / 2).| < 1 by ABSVALUE:def 1;
then (1 / 2) GeoSeq is summable by SERIES_1:24;
then s (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then ((1 / 2) GeoSeq) (#) (FS2 # [p,q]) is summable by A23, SERIES_1:20;
then (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n = 0 by A23, A22, RSSPACE:17;
then A28: (((1 / 2) GeoSeq) . n) * ((FS2 # [p,q]) . n) = 0 by SEQ_1:8;
(1 / 2) |^ n > 0 by NEWTON:83;
then ((1 / 2) GeoSeq) . n <> 0 by PREPOWER:def 1;
then A29: (FS2 # [p,q]) . n = 0 by A28, XCMPLX_1:6;
A30: pmet1 . (p,q) = (dist (pmet1,p)) . q by Def2;
( dom (dist (pmet1,p)) = the carrier of T & q in {q} ) by FUNCT_2:def 1, TARSKI:def 1;
then A31: (dist (pmet1,p)) . q in (dist (pmet1,p)) .: {q} by FUNCT_1:def 6;
( not (dist (pmet1,p)) .: {q} is empty & (dist (pmet1,p)) .: {q} is bounded_below ) by A26, Lm1;
then (dist (pmet1,p)) . q > 0 by A31, A27, SEQ_4:def 2;
hence contradiction by A25, A29, A30, SEQFUNC:def 10; :: thesis:

end;

pmet is_a_pseudometric_of the carrier of T by A2, A5, Th15;
then ( pmet is Reflexive & pmet is discerning & pmet is symmetric & pmet is triangle ) by A18, METRIC_1:def 3, NAGATA_1:def 10;
then A32: pmet is_metric_of the carrier of T by METRIC_6:3;
hence ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) by A5; :: thesis:
for A being non empty Subset of T holds Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }

proof

let A be non empty Subset of T; :: thesis:
set INF = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ;
A33: { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } c= Cl A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis:
then consider p being Point of T such that
A34: x = p and
A35: (lower_bound (pmet,A)) . p = 0 ;
A36: lower_bound ((dist (pmet,p)) .: A) = 0 by A35, Def3;
pmet is_a_pseudometric_of the carrier of T by A2, A5, Th15;
then A37: ( not (dist (pmet,p)) .: A is empty & (dist (pmet,p)) .: A is bounded_below ) by Lm1;
A38: ( A c= Cl A & ex y being object st y in A ) by PRE_TOPC:18, XBOOLE_0:def 1;
A39: A c= Cl A by PRE_TOPC:18;
assume not x in Cl A ; :: thesis:
then consider n being Nat such that
A40: for pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet1 holds
(lower_bound (pmet1,(Cl A))) . p > 0 by A3, A34, A38;
(1 / 2) |^ n > 0 by NEWTON:83;
then A41: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def 1;
(1 / 2) |^ n > 0 by NEWTON:83;
then A42: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def 1;
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A43: FS2 . n = pmet1 and
A44: pmet1 is_a_pseudometric_of the carrier of T and
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and
for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds
pmet19 is continuous by A2;
set r = (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p);
A45: lower_bound ((dist (pmet1,p)) .: (Cl A)) = (lower_bound (pmet1,(Cl A))) . p by Def3;
A46: (lower_bound (pmet1,(Cl A))) . p > 0 by A40, A43;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) > 0 by A41, XREAL_1:129;
then ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 > 0 by XREAL_1:215;
then consider rn being Real such that
A47: rn in (dist (pmet,p)) .: A and
A48: rn < (lower_bound ((dist (pmet,p)) .: A)) + (((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2) by A37, SEQ_4:def 2;
consider a being object such that
A49: a in dom (dist (pmet,p)) and
A50: a in A and
A51: rn = (dist (pmet,p)) . a by A47, FUNCT_1:def 6;
reconsider a = a as Point of T by A49;
reconsider pa = [p,a] as Element of [: the carrier of T, the carrier of T:] ;
A52: (dist (pmet1,p)) . a = pmet1 . (p,a) by Def2;
dom (dist (pmet1,p)) = the carrier of T by FUNCT_2:def 1;
then A53: (dist (pmet1,p)) . a in (dist (pmet1,p)) .: (Cl A) by A50, A39, FUNCT_1:def 6;
( not (dist (pmet1,p)) .: (Cl A) is empty & (dist (pmet1,p)) .: (Cl A) is bounded_below ) by A44, A50, A39, Lm1;
then (lower_bound (pmet1,(Cl A))) . p <= (dist (pmet1,p)) . a by A53, A45, SEQ_4:def 2;
then (lower_bound (pmet1,(Cl A))) . p <= (FS2 # pa) . n by A43, A52, SEQFUNC:def 10;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) <= (((1 / 2) GeoSeq) . n) * ((FS2 # pa) . n) by A42, XREAL_1:64;
then A54: (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) <= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n by SEQ_1:8;
A55: for k being Nat holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . k & (((1 / 2) GeoSeq) (#) (FS2 # pa)) . k <= (s (#) ((1 / 2) GeoSeq)) . k ) by A8;
pmet . pa = pmet . (p,a) ;
then A56: rn = pmet . pa by A51, Def2;
1 / 2 < 1 ;
then |.(1 / 2).| < 1 by ABSVALUE:def 1;
then (1 / 2) GeoSeq is summable by SERIES_1:24;
then s (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then ((1 / 2) GeoSeq) (#) (FS2 # pa) is summable by A55, SERIES_1:20;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n <= Sum (((1 / 2) GeoSeq) (#) (FS2 # pa)) by A55, RSSPACE2:3;
then rn >= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n by A5, A56;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by A48, A36, XXREAL_0:2;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by A54, XXREAL_0:2;
hence contradiction by A41, A46, XREAL_1:129, XREAL_1:216; :: thesis:

end;

Cl A c= { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A57: x in Cl A ; :: thesis:
then reconsider p = x as Point of T ;
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) by A2, A5, Th15;
then (lower_bound (pmet,A)) . p = 0 by A57, Th16;
hence x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis:

end;

hence Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } by A33; :: thesis:

end;

hence T is metrizable by A32, Th10; :: thesis: