for T being non empty TopSpace
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 FS2 # pq is summable ) 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 (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T