let T be 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
set cT = the carrier of T;
let FS2 be Functional_Sequence of [: the carrier of T, the carrier of T:],REAL; ( ( 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 ) implies 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 )
assume that
A1:
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 )
and
A2:
for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable
; 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
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ( ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) implies pmet is_a_pseudometric_of the carrier of T )
assume A3:
for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq)
; pmet is_a_pseudometric_of the carrier of T
now for a, b, c being Point of T holds
( pmet . (a,a) = 0 & pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) )let a,
b,
c be
Point of
T;
( pmet . (a,a) = 0 & pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) )thus
pmet . (
a,
a)
= 0
pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b))thus
pmet . (
a,
c)
<= (pmet . (a,b)) + (pmet . (c,b))
verumproof
set ab =
[a,b];
set cb =
[c,b];
set ac =
[a,c];
set Fac =
FS2 # [a,c];
set Fab =
FS2 # [a,b];
set Fcb =
FS2 # [c,b];
A7:
now for n being Nat holds
( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n )let n be
Nat;
( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n )A8:
(
(FS2 . n) . [a,c] = (FS2 # [a,c]) . n &
(FS2 . n) . [a,b] = (FS2 # [a,b]) . n )
by SEQFUNC:def 10;
consider pmet1 being
Function of
[: the carrier of T, the carrier of T:],
REAL such that A9:
FS2 . n = pmet1
and A10:
pmet1 is_a_pseudometric_of the
carrier of
T
by A1;
A11:
0 <= pmet1 . (
a,
c)
by A10, NAGATA_1:29;
pmet1 . (
a,
c)
<= (pmet1 . (a,b)) + (pmet1 . (c,b))
by A10, NAGATA_1:28;
then
(FS2 # [a,c]) . n <= ((FS2 # [a,b]) . n) + ((FS2 # [c,b]) . n)
by A9, A8, SEQFUNC:def 10;
hence
(
0 <= (FS2 # [a,c]) . n &
(FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n )
by A9, A11, SEQFUNC:def 10, SEQ_1:7;
verum end;
A12:
(
FS2 # [a,b] is
summable &
FS2 # [c,b] is
summable )
by A2;
then
(FS2 # [a,b]) + (FS2 # [c,b]) is
summable
by SERIES_1:7;
then A13:
Sum (FS2 # [a,c]) <= Sum ((FS2 # [a,b]) + (FS2 # [c,b]))
by A7, SERIES_1:20;
A14:
(
Sum (FS2 # [a,b]) = pmet . [a,b] &
Sum (FS2 # [c,b]) = pmet . [c,b] )
by A3;
Sum ((FS2 # [a,b]) + (FS2 # [c,b])) = (Sum (FS2 # [a,b])) + (Sum (FS2 # [c,b]))
by A12, SERIES_1:7;
hence
pmet . (
a,
c)
<= (pmet . (a,b)) + (pmet . (c,b))
by A3, A13, A14;
verum
end; end;
hence
pmet is_a_pseudometric_of the carrier of T
by NAGATA_1:28; verum