let T be non empty TopSpace; :: thesis: for s being Real

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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

set Geo = (1 / 2) GeoSeq ;

set cT = the carrier of T;

set cTT = the carrier of [:T,T:];

let s be Real; :: 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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) )

assume 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 & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ; :: 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

set SGeo = s (#) ((1 / 2) GeoSeq);

deffunc H_{1}( Nat) -> Element of bool [:[: the carrier of T, the carrier of T:],REAL:] = (((1 / 2) GeoSeq) . $1) (#) (FS2 . $1);

consider GeoF being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL such that

A2: for n being Nat holds GeoF . n = H_{1}(n)
from SEQFUNC:sch 1();

the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

then reconsider GeoF9 = GeoF as Functional_Sequence of the carrier of [:T,T:],REAL ;

A3: for pq being Element of [: the carrier of T, the carrier of T:]

for k being Nat holds

( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

pmet9 is continuous ) ) )

assume A23: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ; :: thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

A24: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (GeoF # pq)

( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )

then |.(1 / 2).| < 1 by ABSVALUE:def 1;

then A36: (1 / 2) GeoSeq is summable by SERIES_1:24;

A37: for pq being Element of [: the carrier of T, the carrier of T:]

for pq9 being Point of [:T,T:] st pq = pq9 holds

GeoF # pq = GeoF9 # pq9

( seq is summable & ( for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= seq . n ) )

pmet19 is continuous by A12, A24, A39, Th14;

for pq being Element of [: the carrier of T, the carrier of T:] holds GeoF # pq is summable

pmet9 is continuous ) ) by A25, A24, A40, Th11; :: thesis: verum

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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

set Geo = (1 / 2) GeoSeq ;

set cT = the carrier of T;

set cTT = the carrier of [:T,T:];

let s be Real; :: 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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

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 pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ) 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) )

assume 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 & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) ) ; :: 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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds

( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

set SGeo = s (#) ((1 / 2) GeoSeq);

deffunc H

consider GeoF being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL such that

A2: for n being Nat holds GeoF . n = H

the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

then reconsider GeoF9 = GeoF as Functional_Sequence of the carrier of [:T,T:],REAL ;

A3: for pq being Element of [: the carrier of T, the carrier of T:]

for k being Nat holds

( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

proof

A12:
for n being Nat ex f being RealMap of [:T,T:] st
let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis: for k being Nat holds

( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

let k be Nat; :: thesis: ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

consider x, y being object such that

A4: ( x in the carrier of T & y in the carrier of T ) and

A5: [x,y] = pq by ZFMISC_1:def 2;

reconsider x = x, y = y as Point of T by A4;

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A6: FS2 . k = pmet1 and

A7: pmet1 is_a_pseudometric_of the carrier of T and

A8: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

A9: 0 <= pmet1 . (x,y) by A7, NAGATA_1:29;

dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by A6, FUNCT_2:def 1;

then A10: (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5

.= (GeoF . k) . pq by A2

.= (GeoF # pq) . k by SEQFUNC:def 10 ;

(1 / 2) |^ k > 0 by NEWTON:83;

then A11: ((1 / 2) GeoSeq) . k > 0 by PREPOWER:def 1;

then (((1 / 2) GeoSeq) . k) * (pmet1 . pq) <= (((1 / 2) GeoSeq) . k) * s by A8, XREAL_1:64;

hence ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k ) by A6, A5, A10, A9, A11, SEQ_1:9; :: thesis: verum

end;( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

let k be Nat; :: thesis: ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k )

consider x, y being object such that

A4: ( x in the carrier of T & y in the carrier of T ) and

A5: [x,y] = pq by ZFMISC_1:def 2;

reconsider x = x, y = y as Point of T by A4;

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A6: FS2 . k = pmet1 and

A7: pmet1 is_a_pseudometric_of the carrier of T and

A8: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

A9: 0 <= pmet1 . (x,y) by A7, NAGATA_1:29;

dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by A6, FUNCT_2:def 1;

then A10: (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5

.= (GeoF . k) . pq by A2

.= (GeoF # pq) . k by SEQFUNC:def 10 ;

(1 / 2) |^ k > 0 by NEWTON:83;

then A11: ((1 / 2) GeoSeq) . k > 0 by PREPOWER:def 1;

then (((1 / 2) GeoSeq) . k) * (pmet1 . pq) <= (((1 / 2) GeoSeq) . k) * s by A8, XREAL_1:64;

hence ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k ) by A6, A5, A10, A9, A11, SEQ_1:9; :: thesis: verum

( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

proof

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 (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) implies ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
let n be Nat; :: thesis: ex f being RealMap of [:T,T:] st

( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A13: FS2 . n = pmet1 and

pmet1 is_a_pseudometric_of the carrier of T and

for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

A14: for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

then reconsider pmet19 = pmet1 as RealMap of [:T,T:] ;

reconsider pR = pmet19 as Function of [:T,T:],R^1 by TOPMETR:17;

pmet19 is continuous by A14;

then pR is continuous by JORDAN5A:27;

then consider fR being Function of [:T,T:],R^1 such that

A15: for pq9 being Point of [:T,T:]

for rn being Real st pR . pq9 = rn holds

fR . pq9 = (((1 / 2) GeoSeq) . n) * rn and

A16: fR is continuous by JGRAPH_2:23;

reconsider f = fR as RealMap of [:T,T:] by TOPMETR:17;

A17: dom f = the carrier of [:T,T:] by FUNCT_2:def 1;

take f ; :: thesis: ( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

A18: dom pmet1 = [: the carrier of T, the carrier of T:] by FUNCT_2:def 1;

A19: GeoF9 . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;

then A20: dom (FS2 . n) = dom (GeoF9 . n) by VALUED_1:def 5;

A21: [: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;

end;( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A13: FS2 . n = pmet1 and

pmet1 is_a_pseudometric_of the carrier of T and

for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

A14: for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

then reconsider pmet19 = pmet1 as RealMap of [:T,T:] ;

reconsider pR = pmet19 as Function of [:T,T:],R^1 by TOPMETR:17;

pmet19 is continuous by A14;

then pR is continuous by JORDAN5A:27;

then consider fR being Function of [:T,T:],R^1 such that

A15: for pq9 being Point of [:T,T:]

for rn being Real st pR . pq9 = rn holds

fR . pq9 = (((1 / 2) GeoSeq) . n) * rn and

A16: fR is continuous by JGRAPH_2:23;

reconsider f = fR as RealMap of [:T,T:] by TOPMETR:17;

A17: dom f = the carrier of [:T,T:] by FUNCT_2:def 1;

take f ; :: thesis: ( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )

A18: dom pmet1 = [: the carrier of T, the carrier of T:] by FUNCT_2:def 1;

A19: GeoF9 . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;

then A20: dom (FS2 . n) = dom (GeoF9 . n) by VALUED_1:def 5;

A21: [: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;

A22: now :: thesis: for pq9 being Point of [:T,T:] st pq9 in dom (GeoF9 . n) holds

(GeoF9 . n) . pq9 = f . pq9

(GeoF9 . n) . pq9 = f . pq9

let pq9 be Point of [:T,T:]; :: thesis: ( pq9 in dom (GeoF9 . n) implies (GeoF9 . n) . pq9 = f . pq9 )

assume pq9 in dom (GeoF9 . n) ; :: thesis: (GeoF9 . n) . pq9 = f . pq9

(GeoF9 . n) . pq9 = (((1 / 2) GeoSeq) . n) * (pmet1 . pq9) by A13, A19, A20, A18, A21, VALUED_1:def 5;

hence (GeoF9 . n) . pq9 = f . pq9 by A15; :: thesis: verum

end;assume pq9 in dom (GeoF9 . n) ; :: thesis: (GeoF9 . n) . pq9 = f . pq9

(GeoF9 . n) . pq9 = (((1 / 2) GeoSeq) . n) * (pmet1 . pq9) by A13, A19, A20, A18, A21, VALUED_1:def 5;

hence (GeoF9 . n) . pq9 = f . pq9 by A15; :: thesis: verum

now :: thesis: for pq9 being Point of [:T,T:] holds f . pq9 >= 0

hence
( GeoF9 . n = f & f is continuous & ( for pq9 being Point of [:T,T:] holds f . pq9 >= 0 ) )
by A13, A16, A20, A18, A17, A21, A22, JORDAN5A:27, PARTFUN1:5; :: thesis: verumlet pq9 be Point of [:T,T:]; :: thesis: f . pq9 >= 0

reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

( (GeoF9 . n) . pq9 = (GeoF # pq) . n & (GeoF # pq) . n >= 0 ) by A3, SEQFUNC:def 10;

hence f . pq9 >= 0 by A13, A20, A18, A22; :: thesis: verum

end;reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

( (GeoF9 . n) . pq9 = (GeoF # pq) . n & (GeoF # pq) . n >= 0 ) by A3, SEQFUNC:def 10;

hence f . pq9 >= 0 by A13, A20, A18, A22; :: thesis: verum

pmet9 is continuous ) ) )

assume A23: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ; :: thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous ) )

A24: for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (GeoF # pq)

proof

A25:
for n being Nat ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st
let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis: pmet . pq = Sum (GeoF # pq)

hence pmet . pq = Sum (GeoF # pq) by A23; :: thesis: verum

end;now :: thesis: for z being object st z in NAT holds

(((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z

then
((1 / 2) GeoSeq) (#) (FS2 # pq) = GeoF # pq
;(((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z

let z be object ; :: thesis: ( z in NAT implies (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z )

assume z in NAT ; :: thesis: (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z

then reconsider k = z as Element of NAT ;

ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st

( FS2 . k = pmet1 & pmet1 is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s ) & ( for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous ) ) by A1;

then dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by FUNCT_2:def 1;

then (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5

.= (GeoF . k) . pq by A2

.= (GeoF # pq) . k by SEQFUNC:def 10 ;

then (GeoF # pq) . k = (((1 / 2) GeoSeq) . k) * ((FS2 # pq) . k) by SEQFUNC:def 10

.= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . k by SEQ_1:8 ;

hence (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z ; :: thesis: verum

end;assume z in NAT ; :: thesis: (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z

then reconsider k = z as Element of NAT ;

ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st

( FS2 . k = pmet1 & pmet1 is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s ) & ( for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous ) ) by A1;

then dom ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) = [: the carrier of T, the carrier of T:] by FUNCT_2:def 1;

then (((1 / 2) GeoSeq) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5

.= (GeoF . k) . pq by A2

.= (GeoF # pq) . k by SEQFUNC:def 10 ;

then (GeoF # pq) . k = (((1 / 2) GeoSeq) . k) * ((FS2 # pq) . k) by SEQFUNC:def 10

.= (((1 / 2) GeoSeq) (#) (FS2 # pq)) . k by SEQ_1:8 ;

hence (((1 / 2) GeoSeq) (#) (FS2 # pq)) . z = (GeoF # pq) . z ; :: thesis: verum

hence pmet . pq = Sum (GeoF # pq) by A23; :: thesis: verum

( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )

proof

1 / 2 < 1
;
let n be Nat; :: thesis: ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st

( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A26: FS2 . n = pmet1 and

A27: pmet1 is_a_pseudometric_of the carrier of T and

for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

deffunc H_{2}( Element of the carrier of T, Element of the carrier of T) -> Element of REAL = (((1 / 2) GeoSeq) . n) * (pmet1 . ($1,$2));

consider GF being Function of [: the carrier of T, the carrier of T:],REAL such that

A28: for p, q being Point of T holds GF . (p,q) = H_{2}(p,q)
from BINOP_1:sch 4();

A32: GeoF . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;

then A33: dom (FS2 . n) = dom (GeoF . n) by VALUED_1:def 5;

hence ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st

( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T ) by A26, A33, A34, A31, BINOP_1:20; :: thesis: verum

end;( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T )

consider pmet1 being Function of [: the carrier of T, the carrier of T:],REAL such that

A26: FS2 . n = pmet1 and

A27: pmet1 is_a_pseudometric_of the carrier of T and

for pq being Element of [: the carrier of T, the carrier of T:] holds pmet1 . pq <= s and

for pmet19 being RealMap of [:T,T:] st pmet1 = pmet19 holds

pmet19 is continuous by A1;

deffunc H

consider GF being Function of [: the carrier of T, the carrier of T:],REAL such that

A28: for p, q being Point of T holds GF . (p,q) = H

now :: thesis: for a, b, c being Point of T holds

( GF . (a,a) = 0 & GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) )

then A31:
GF is_a_pseudometric_of the carrier of T
by NAGATA_1:28;( GF . (a,a) = 0 & GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) )

let a, b, c be Point of T; :: thesis: ( GF . (a,a) = 0 & GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) )

(1 / 2) |^ n > 0 by NEWTON:83;

then A29: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def 1;

pmet1 . (a,c) <= (pmet1 . (a,b)) + (pmet1 . (c,b)) by A27, NAGATA_1:28;

then (pmet1 . (a,c)) * (((1 / 2) GeoSeq) . n) <= ((pmet1 . (a,b)) + (pmet1 . (c,b))) * (((1 / 2) GeoSeq) . n) by A29, XREAL_1:64;

then A30: GF . (a,c) <= ((((1 / 2) GeoSeq) . n) * (pmet1 . (a,b))) + ((((1 / 2) GeoSeq) . n) * (pmet1 . (c,b))) by A28;

( GF . (a,a) = (((1 / 2) GeoSeq) . n) * (pmet1 . (a,a)) & pmet1 . (a,a) = 0 ) by A27, A28, NAGATA_1:28;

hence GF . (a,a) = 0 ; :: thesis: GF . (a,c) <= (GF . (a,b)) + (GF . (c,b))

(((1 / 2) GeoSeq) . n) * (pmet1 . (a,b)) = GF . (a,b) by A28;

hence GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) by A28, A30; :: thesis: verum

end;(1 / 2) |^ n > 0 by NEWTON:83;

then A29: ((1 / 2) GeoSeq) . n > 0 by PREPOWER:def 1;

pmet1 . (a,c) <= (pmet1 . (a,b)) + (pmet1 . (c,b)) by A27, NAGATA_1:28;

then (pmet1 . (a,c)) * (((1 / 2) GeoSeq) . n) <= ((pmet1 . (a,b)) + (pmet1 . (c,b))) * (((1 / 2) GeoSeq) . n) by A29, XREAL_1:64;

then A30: GF . (a,c) <= ((((1 / 2) GeoSeq) . n) * (pmet1 . (a,b))) + ((((1 / 2) GeoSeq) . n) * (pmet1 . (c,b))) by A28;

( GF . (a,a) = (((1 / 2) GeoSeq) . n) * (pmet1 . (a,a)) & pmet1 . (a,a) = 0 ) by A27, A28, NAGATA_1:28;

hence GF . (a,a) = 0 ; :: thesis: GF . (a,c) <= (GF . (a,b)) + (GF . (c,b))

(((1 / 2) GeoSeq) . n) * (pmet1 . (a,b)) = GF . (a,b) by A28;

hence GF . (a,c) <= (GF . (a,b)) + (GF . (c,b)) by A28, A30; :: thesis: verum

A32: GeoF . n = (((1 / 2) GeoSeq) . n) (#) (FS2 . n) by A2;

then A33: dom (FS2 . n) = dom (GeoF . n) by VALUED_1:def 5;

A34: now :: thesis: for x, y being object st [x,y] in dom (GeoF . n) holds

(GeoF . n) . (x,y) = GF . (x,y)

( dom pmet1 = [: the carrier of T, the carrier of T:] & dom GF = [: the carrier of T, the carrier of T:] )
by FUNCT_2:def 1;(GeoF . n) . (x,y) = GF . (x,y)

let x, y be object ; :: thesis: ( [x,y] in dom (GeoF . n) implies (GeoF . n) . (x,y) = GF . (x,y) )

assume A35: [x,y] in dom (GeoF . n) ; :: thesis: (GeoF . n) . (x,y) = GF . (x,y)

then reconsider x9 = x, y9 = y as Point of T by ZFMISC_1:87;

GF . (x9,y9) = (((1 / 2) GeoSeq) . n) * (pmet1 . (x9,y9)) by A28;

hence (GeoF . n) . (x,y) = GF . (x,y) by A26, A32, A35, VALUED_1:def 5; :: thesis: verum

end;assume A35: [x,y] in dom (GeoF . n) ; :: thesis: (GeoF . n) . (x,y) = GF . (x,y)

then reconsider x9 = x, y9 = y as Point of T by ZFMISC_1:87;

GF . (x9,y9) = (((1 / 2) GeoSeq) . n) * (pmet1 . (x9,y9)) by A28;

hence (GeoF . n) . (x,y) = GF . (x,y) by A26, A32, A35, VALUED_1:def 5; :: thesis: verum

hence ex pmet1 being Function of [: the carrier of T, the carrier of T:],REAL st

( GeoF . n = pmet1 & pmet1 is_a_pseudometric_of the carrier of T ) by A26, A33, A34, A31, BINOP_1:20; :: thesis: verum

then |.(1 / 2).| < 1 by ABSVALUE:def 1;

then A36: (1 / 2) GeoSeq is summable by SERIES_1:24;

A37: for pq being Element of [: the carrier of T, the carrier of T:]

for pq9 being Point of [:T,T:] st pq = pq9 holds

GeoF # pq = GeoF9 # pq9

proof

A39:
ex seq being Real_Sequence st
let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis: for pq9 being Point of [:T,T:] st pq = pq9 holds

GeoF # pq = GeoF9 # pq9

let pq9 be Point of [:T,T:]; :: thesis: ( pq = pq9 implies GeoF # pq = GeoF9 # pq9 )

assume A38: pq = pq9 ; :: thesis: GeoF # pq = GeoF9 # pq9

end;GeoF # pq = GeoF9 # pq9

let pq9 be Point of [:T,T:]; :: thesis: ( pq = pq9 implies GeoF # pq = GeoF9 # pq9 )

assume A38: pq = pq9 ; :: thesis: GeoF # pq = GeoF9 # pq9

now :: thesis: for x being Element of NAT holds (GeoF # pq) . x = (GeoF9 # pq9) . x

hence
GeoF # pq = GeoF9 # pq9
; :: thesis: verumlet x be Element of NAT ; :: thesis: (GeoF # pq) . x = (GeoF9 # pq9) . x

(GeoF # pq) . x = (GeoF . x) . pq by SEQFUNC:def 10;

hence (GeoF # pq) . x = (GeoF9 # pq9) . x by A38, SEQFUNC:def 10; :: thesis: verum

end;(GeoF # pq) . x = (GeoF . x) . pq by SEQFUNC:def 10;

hence (GeoF # pq) . x = (GeoF9 # pq9) . x by A38, SEQFUNC:def 10; :: thesis: verum

( seq is summable & ( for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= seq . n ) )

proof

A40:
for pmet19 being RealMap of [:T,T:] st pmet = pmet19 holds
take
s (#) ((1 / 2) GeoSeq)
; :: thesis: ( s (#) ((1 / 2) GeoSeq) is summable & ( for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) )

thus s (#) ((1 / 2) GeoSeq) is summable by A36, SERIES_1:10; :: thesis: for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ; :: thesis: verum

end;for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ) )

thus s (#) ((1 / 2) GeoSeq) is summable by A36, SERIES_1:10; :: thesis: for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

now :: thesis: for n being Nat

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

hence
for n being Natfor pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

let n be Nat; :: thesis: for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

let pq9 be Point of [:T,T:]; :: thesis: (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

(GeoF9 # pq9) . n = (GeoF # pq) . n by A37;

hence (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n by A3; :: thesis: verum

end;let pq9 be Point of [:T,T:]; :: thesis: (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n

reconsider pq = pq9 as Element of [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;

(GeoF9 # pq9) . n = (GeoF # pq) . n by A37;

hence (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n by A3; :: thesis: verum

for pq9 being Point of [:T,T:] holds (GeoF9 # pq9) . n <= (s (#) ((1 / 2) GeoSeq)) . n ; :: thesis: verum

pmet19 is continuous by A12, A24, A39, Th14;

for pq being Element of [: the carrier of T, the carrier of T:] holds GeoF # pq is summable

proof

hence
( pmet is_a_pseudometric_of the carrier of T & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis: GeoF # pq is summable

for k being Nat holds

( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k & s (#) ((1 / 2) GeoSeq) is summable ) by A3, A36, SERIES_1:10;

hence GeoF # pq is summable by SERIES_1:20; :: thesis: verum

end;for k being Nat holds

( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq)) . k & s (#) ((1 / 2) GeoSeq) is summable ) by A3, A36, SERIES_1:10;

hence GeoF # pq is summable by SERIES_1:20; :: thesis: verum

pmet9 is continuous ) ) by A25, A24, A40, Th11; :: thesis: verum