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

( 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)) )

hence
pmet is_a_pseudometric_of the carrier of T
by NAGATA_1:28; :: thesis: verum( 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))

end;thus pmet . (a,a) = 0 :: thesis: pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b))

proof

thus
pmet . (a,c) <= (pmet . (a,b)) + (pmet . (c,b))
:: thesis: verum
set aa = [a,a];

set F = FS2 # [a,a];

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;set F = FS2 # [a,a];

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

then A6:
FS2 # [a,a] = 0 (#) (FS2 # [a,a])
by SEQ_1:9;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;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

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

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];

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;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 )

A12:
( FS2 # [a,b] is summable & FS2 # [c,b] is summable )
by A2;( 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;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

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