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 & pmet1 is_a_pseudometric_of the carrier of T ) by A1;
pmet1 . a,a = 0 by A4, NAGATA_1:28;
hence (FS2 # [a,a]) . n = 0 * ((FS2 # [a,a]) . n) by A4, SEQFUNC:def 11; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n )
consider pmet1 being Function of [:the carrier of T,the carrier of T:],REAL such that
A6: ( FS2 . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T ) by A1;
( pmet1 . a,c <= (pmet1 . a,b) + (pmet1 . c,b) & 0 <= pmet1 . a,c & pmet1 . c,b = pmet1 . [c,b] & pmet1 . a,c = pmet1 . [a,c] ) by A6, NAGATA_1:28, NAGATA_1:29;
then ( 0 <= (FS2 . n) . [a,c] & (FS2 . n) . [a,c] <= ((FS2 . n) . [a,b]) + ((FS2 . n) . [c,b]) & (FS2 . n) . [a,c] = (FS2 # [a,c]) . n & (FS2 . n) . [a,b] = (FS2 # [a,b]) . n ) by A6, SEQFUNC:def 11;
then ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) . n) + ((FS2 # [c,b]) . n) ) by SEQFUNC:def 11;
hence ( 0 <= (FS2 # [a,c]) . n & (FS2 # [a,c]) . n <= ((FS2 # [a,b]) + (FS2 # [c,b])) . n ) by SEQ_1:11; :: thesis: verum

end;

then ( Sum (FS2 # [a,c]) <= Sum ((FS2 # [a,b]) + (FS2 # [c,b])) & Sum (FS2 # [a,b]) = pmet . [a,b] & Sum (FS2 # [c,b]) = pmet . [c,b] & pmet . [a,b] = pmet . a,b & pmet . [c,b] = pmet . c,b ) by A3, A5, SERIES_1:24;
hence pmet . a,c <= (pmet . a,b) + (pmet . c,b) by A3, A5; :: thesis: verum

end;

end;

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