let T be non empty TopSpace; :: 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 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; :: 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 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 ; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: pmet is_a_pseudometric_of the carrier of T

now :: thesis: 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; :: thesis: ( pmet . (a,a) = 0 & pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) )
thus pmet . (a,a) = 0 :: thesis: pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b))

proof

set aa = [a,a];
set F = FS2 # [a,a];

now :: thesis: for n being Nat holds (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n)

let n be Nat; :: thesis: (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n)
consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that
A4: FS2 . n = pmet1 and
A5: pmet1 is_a_pseudometric_of the carrier of T by A1;
pmet1 . (a,a) = 0 by A5, NAGATA_1:28;
hence (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n) by A4, SEQFUNC:def 10; :: thesis: verum

end;

then A6: FS2 # [a,a] = 0 (#) (FS2 # [a,a]) by SEQ_1:9;
FS2 # [a,a] is summable by A2;
then Sum (FS2 # [a,a]) = 0 * (Sum (FS2 # [a,a])) by A6, SERIES_1:10;
hence pmet . (a,a) = 0 by A3; :: thesis: verum

end;

thus pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b)) :: thesis: verum

proof

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

end;

end;

hence pmet is_a_pseudometric_of the carrier of T by NAGATA_1:28; :: thesis: verum