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 Element of 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 Element of 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 Element of 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

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

let n be Element of 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 11; :: thesis: verum

end;

then A6: FS2 # [a,a] = 0 (#) (FS2 # [a,a]) by SEQ_1:13;
FS2 # [a,a] is summable by A2;
then Sum (FS2 # [a,a]) = 0 * (Sum (FS2 # [a,a])) by A6, SERIES_1:13;
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

let n be Element of 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 11;
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 11;
hence ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n ) by A9, A11, SEQFUNC:def 11, SEQ_1:11; :: 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:10;
then A13: Sum (FS2 # [a,c]) <= Sum ((FS2 # [a,b]) + (FS2 # [c,b])) by A7, SERIES_1:24;
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:10;
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