theorem Th15:
for
T being non
empty TopSpace 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 ) ) ) holds
for
pmet being
Function of
[: the carrier of T, the carrier of T:],
REAL st ( for
pq being
Element of
[: the carrier of T, the carrier of T:] holds
pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
(
pmet is_a_pseudometric_of the
carrier of
T & ( for
pmet9 being
RealMap of
[:T,T:] st
pmet = pmet9 holds
pmet9 is
continuous ) )