let T be non empty TopSpace; :: thesis: ( T is T_1 implies for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( 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 ) ) ) & ( 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 ) holds
( 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)) ) ) & T is metrizable ) )

assume A1: T is T_1 ; :: thesis: for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( 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 ) ) ) & ( 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 ) holds
( 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)) ) ) & T is metrizable )

set cT = the carrier of T;
set Geo = (1 / 2) GeoSeq ;
let s be Real; :: thesis: for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( 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 ) ) ) & ( 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 ) holds
( 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)) ) ) & T is metrizable )

let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( ( 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 ) ) ) & ( 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 ) implies ( 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)) ) ) & T is metrizable ) )

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: ( 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)) ) ) & T is metrizable )

deffunc H1( 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) = H1(p,q) from 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: pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq))
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
.= H1(p,q) by A4 ;
hence pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) by A7; :: thesis: verum
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: for n being Nat holds
( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )

let n be Nat; :: thesis: ( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )
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 ;
A17: pmet1 . pq = (FS2 # pq) . n by ;
then (((1 / 2) GeoSeq) . n) * ((FS2 # pq) . n) <= (((1 / 2) GeoSeq) . n) * s by ;
hence ( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) by ; :: thesis: verum
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: ( pmet . (p,q) = 0 implies p = q )
assume that
A19: pmet . (p,q) = 0 and
A20: p <> q ; :: thesis: contradiction
set Q = {q};
A21: not p in {q} by ;
set pq = [p,q];
A22: Sum (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) = 0 by ;
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 ;
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 ;
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 ;
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 ;
then (((1 / 2) GeoSeq) (#) (FS2 # [p,q])) . n = 0 by ;
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 ;
A30: pmet1 . (p,q) = (dist (pmet1,p)) . q by Def2;
( dom (dist (pmet1,p)) = the carrier of T & q in {q} ) by ;
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 ;
then (dist (pmet1,p)) . q > 0 by ;
hence contradiction by A25, A29, A30, SEQFUNC:def 10; :: thesis: verum
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 ;
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: T is metrizable
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: Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
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: ( not x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } or x in Cl A )
assume x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: x in Cl A
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 ;
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 ;
A39: A c= Cl A by PRE_TOPC:18;
assume not x in Cl A ; :: thesis: contradiction
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 ;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) > 0 by ;
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 ;
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 ;
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 ;
( 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 ;
then (lower_bound (pmet1,(Cl A))) . p <= (FS2 # pa) . n by ;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) <= (((1 / 2) GeoSeq) . n) * ((FS2 # pa) . n) by ;
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 ;
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 ;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n <= Sum (((1 / 2) GeoSeq) (#) (FS2 # pa)) by ;
then rn >= (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n by ;
then (((1 / 2) GeoSeq) (#) (FS2 # pa)) . n < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by ;
then (((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p) < ((((1 / 2) GeoSeq) . n) * ((lower_bound (pmet1,(Cl A))) . p)) / 2 by ;
hence contradiction by A41, A46, XREAL_1:129, XREAL_1:216; :: thesis: verum
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: ( not x in Cl A or x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } )
assume A57: x in Cl A ; :: thesis: x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
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 ;
hence x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: verum
end;
hence Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } by A33; :: thesis: verum
end;
hence T is metrizable by ; :: thesis: verum