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 H_{1}( 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_{1}(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))

for n being Nat holds

( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )

p = q

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: 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 }

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 H

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

A5: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq))

proof

A8:
for pq being Element of [: the carrier of T, the carrier of T:]
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

.= H_{1}(p,q)
by A4
;

hence pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) by A7; :: thesis: verum

end;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

hence pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) by A7; :: thesis: verum

for n being Nat holds

( 0 <= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n & (((1 / 2) GeoSeq) (#) (FS2 # pq)) . n <= (s (#) ((1 / 2) GeoSeq)) . n )

proof

A18:
for p, q being Point of T st pmet . (p,q) = 0 holds
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 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: verum

end;( 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 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: verum

p = q

proof

pmet is_a_pseudometric_of the carrier of T
by A2, A5, Th15;
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 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: verum

end;assume that

A19: pmet . (p,q) = 0 and

A20: p <> q ; :: thesis: contradiction

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: verum

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: 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

hence
T is metrizable
by A32, Th10; :: thesis: verum
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

end;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

Cl A c= { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
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 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: 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 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: verum

end;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 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: 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 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: verum

proof

hence
Cl A = { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 }
by A33; :: thesis: verum
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 A57, Th16;

hence x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: verum

end;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 A57, Th16;

hence x in { p where p is Point of T : (lower_bound (pmet,A)) . p = 0 } ; :: thesis: verum