theorem Th17:
for
T being non
empty TopSpace st
T is
T_1 holds
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 )