let T be non empty TopSpace; :: thesis:
set cT = the carrier of T;
set cTT = the carrier of [:T,T:];
set Geo = (1 / 2) GeoSeq ;
let s be Real; :: thesis:
let FS2 be Functional_Sequence of [:the carrier of T,the carrier of T:],REAL ; :: thesis:
assume 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 & ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq <= s ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) ) ; :: thesis:
let pmet be Function of [:the carrier of T,the carrier of T:],REAL ; :: thesis:
assume A2: for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq ) (#) (FS2 # pq)) ; :: thesis:
deffunc H₁( 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
A3: for n being Nat holds GeoF . n = H₁(n) from SEQFUNC:sch 1();
A4: for n being Element of NAT 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 )

proof

let n be Element of NAT ; :: thesis:
consider pmet1 being Function of [:the carrier of T,the carrier of T:],REAL such that
A5: ( FS2 . n = 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 pmet1' being RealMap of [:T,T:] st pmet1 = pmet1' holds
pmet1' is continuous ) ) by A1;
deffunc H₂( 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
A6: for p, q being Point of T holds GF . p,q = H₂(p,q) from BINOP_1:sch 4();
A7: GeoF . n = GF

proof

A8: GeoF . n = (((1 / 2) GeoSeq ) . n) (#) (FS2 . n) by A3;
then A9: ( dom (FS2 . n) = dom (GeoF . n) & 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, VALUED_1:def 5;

now

let x, y be set ; :: thesis:
assume A10: [x,y] in dom (GeoF . n) ; :: thesis:
then reconsider x' = x, y' = y as Point of T by ZFMISC_1:106;
( (GeoF . n) . x,y = (((1 / 2) GeoSeq ) . n) * (pmet1 . [x,y]) & GF . x',y' = (((1 / 2) GeoSeq ) . n) * (pmet1 . x',y') ) by A5, A6, A8, A10, VALUED_1:def 5;
hence (GeoF . n) . x,y = GF . x,y ; :: thesis:

end;

hence GeoF . n = GF by A5, A9, BINOP_1:32; :: thesis:

end;

GF is_a_pseudometric_of the carrier of T

proof

now

let a, b, c be Point of T; :: thesis:
thus GF . a,a = 0 :: thesis:

proof

( GF . a,a = (((1 / 2) GeoSeq ) . n) * (pmet1 . a,a) & pmet1 . a,a = 0 ) by A5, A6, NAGATA_1:28;
hence GF . a,a = 0 ; :: thesis:

end;

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

proof

(1 / 2) |^ n > 0 by NEWTON:102;
then ( pmet1 . a,c <= (pmet1 . a,b) + (pmet1 . c,b) & ((1 / 2) GeoSeq ) . n > 0 ) by A5, NAGATA_1:28, PREPOWER:def 1;
then (pmet1 . a,c) * (((1 / 2) GeoSeq ) . n) <= ((pmet1 . a,b) + (pmet1 . c,b)) * (((1 / 2) GeoSeq ) . n) by XREAL_1:66;
then ( GF . a,c <= ((((1 / 2) GeoSeq ) . n) * (pmet1 . a,b)) + ((((1 / 2) GeoSeq ) . n) * (pmet1 . c,b)) & (((1 / 2) GeoSeq ) . n) * (pmet1 . a,b) = GF . a,b & (((1 / 2) GeoSeq ) . n) * (pmet1 . c,b) = GF . c,b ) by A6;
hence GF . a,c <= (GF . a,b) + (GF . c,b) ; :: thesis:

end;

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

end;

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 A7; :: thesis:

end;

set SGeo = s (#) ((1 / 2) GeoSeq );
A11: for pq being Element of [:the carrier of T,the carrier of T:]
for k being Element of NAT holds
( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq )) . k )

proof

let pq be Element of [:the carrier of T,the carrier of T:]; :: thesis:
let k be Element of NAT ; :: thesis:
consider pmet1 being Function of [:the carrier of T,the carrier of T:],REAL such that
A12: ( 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 pmet1' being RealMap of [:T,T:] st pmet1 = pmet1' holds
pmet1' is continuous ) ) by A1;
consider x, y being set such that
A13: ( x in the carrier of T & y in the carrier of T & [x,y] = pq ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Point of T by A13;
dom (FS2 . k) = [:the carrier of T,the carrier of T:] by A12, FUNCT_2:def 1;
then dom ((((1 / 2) GeoSeq ) . k) (#) (FS2 . k)) = [:the carrier of T,the carrier of T:] by VALUED_1:def 5;
then A14: (((1 / 2) GeoSeq ) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq ) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5
.= (GeoF . k) . pq by A3
.= (GeoF # pq) . k by SEQFUNC:def 11 ;
(1 / 2) |^ k > 0 by NEWTON:102;
then ( 0 <= pmet1 . x,y & pmet1 . pq <= s & pmet1 . x,y = pmet1 . pq & ((1 / 2) GeoSeq ) . k > 0 ) by A12, A13, NAGATA_1:29, PREPOWER:def 1;
then ( 0 <= (((1 / 2) GeoSeq ) . k) * (pmet1 . pq) & (((1 / 2) GeoSeq ) . k) * (pmet1 . pq) <= (((1 / 2) GeoSeq ) . k) * s ) by XREAL_1:66;
hence ( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq )) . k ) by A12, A14, SEQ_1:13; :: thesis:

end;

( 0 < 1 / 2 & 1 / 2 < 1 ) ;
then abs (1 / 2) < 1 by ABSVALUE:def 1;
then A15: (1 / 2) GeoSeq is summable by SERIES_1:28;
A16: for pq being Element of [:the carrier of T,the carrier of T:] holds GeoF # pq is summable

proof

let pq be Element of [:the carrier of T,the carrier of T:]; :: thesis:
for k being Element of NAT holds
( 0 <= (GeoF # pq) . k & (GeoF # pq) . k <= (s (#) ((1 / 2) GeoSeq )) . k & s (#) ((1 / 2) GeoSeq ) is summable ) by A11, A15, SERIES_1:13;
hence GeoF # pq is summable by SERIES_1:24; :: thesis:

end;

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

proof

let pq be Element of [:the carrier of T,the carrier of T:]; :: thesis:

now

let z be set ; :: thesis:
assume z in NAT ; :: thesis:
then reconsider k = z as Element of NAT ;
consider pmet1 being Function of [:the carrier of T,the carrier of T:],REAL such that
A18: ( 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 pmet1' being RealMap of [:T,T:] st pmet1 = pmet1' holds
pmet1' is continuous ) ) by A1;
dom (FS2 . k) = [:the carrier of T,the carrier of T:] by A18, FUNCT_2:def 1;
then dom ((((1 / 2) GeoSeq ) . k) (#) (FS2 . k)) = [:the carrier of T,the carrier of T:] by VALUED_1:def 5;
then (((1 / 2) GeoSeq ) . k) * ((FS2 . k) . pq) = ((((1 / 2) GeoSeq ) . k) (#) (FS2 . k)) . pq by VALUED_1:def 5
.= (GeoF . k) . pq by A3
.= (GeoF # pq) . k by SEQFUNC:def 11 ;
then (GeoF # pq) . k = (((1 / 2) GeoSeq ) . k) * ((FS2 # pq) . k) by SEQFUNC:def 11
.= (((1 / 2) GeoSeq ) (#) (FS2 # pq)) . k by SEQ_1:12 ;
hence (((1 / 2) GeoSeq ) (#) (FS2 # pq)) . z = (GeoF # pq) . z ; :: thesis:

end;

then ((1 / 2) GeoSeq ) (#) (FS2 # pq) = GeoF # pq by FUNCT_2:18;
hence pmet . pq = Sum (GeoF # pq) by A2; :: thesis:

end;

the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then reconsider GeoF' = GeoF as Functional_Sequence of the carrier of [:T,T:],REAL ;
A19: for pq being Element of [:the carrier of T,the carrier of T:]
for pq' being Point of [:T,T:] st pq = pq' holds
GeoF # pq = GeoF' # pq'

proof

let pq be Element of [:the carrier of T,the carrier of T:]; :: thesis:
let pq' be Point of [:T,T:]; :: thesis:
assume A20: pq = pq' ; :: thesis:

now

let x be Element of NAT ; :: thesis:
( (GeoF # pq) . x = (GeoF . x) . pq & (GeoF' # pq') . x = (GeoF' . x) . pq' ) by SEQFUNC:def 11;
hence (GeoF # pq) . x = (GeoF' # pq') . x by A20; :: thesis:

end;

hence GeoF # pq = GeoF' # pq' by FUNCT_2:113; :: thesis:

end;

A22: for n being Element of NAT ex f being RealMap of [:T,T:] st
( GeoF' . n = f & f is continuous & ( for pq' being Point of [:T,T:] holds f . pq' >= 0 ) )

proof

let n be Element of NAT ; :: thesis:
consider pmet1 being Function of [:the carrier of T,the carrier of T:],REAL such that
A23: ( FS2 . n = 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 pmet1' being RealMap of [:T,T:] st pmet1 = pmet1' holds
pmet1' is continuous ) ) by A1;
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then reconsider pmet1' = pmet1 as RealMap of [:T,T:] ;
reconsider pR = pmet1' as Function of [:T,T:],R^1 by TOPMETR:24;
pmet1' is continuous by A23;
then pR is continuous by TOPREAL6:83;
then consider fR being Function of [:T,T:],R^1 such that
A24: ( ( for pq' being Point of [:T,T:]
for rn being real number st pR . pq' = rn holds
fR . pq' = (((1 / 2) GeoSeq ) . n) * rn ) & fR is continuous ) by JGRAPH_2:33;
reconsider f = fR as RealMap of [:T,T:] by TOPMETR:24;
A25: GeoF' . n = (((1 / 2) GeoSeq ) . n) (#) (FS2 . n) by A3;
then A26: ( dom (FS2 . n) = dom (GeoF' . n) & dom pmet1 = [:the carrier of T,the carrier of T:] & dom f = the carrier of [:T,T:] & [:the carrier of T,the carrier of T:] = the carrier of [:T,T:] ) by BORSUK_1:def 5, FUNCT_2:def 1, VALUED_1:def 5;

A27: now

let pq' be Point of [:T,T:]; :: thesis:
assume pq' in dom (GeoF' . n) ; :: thesis:
( (GeoF' . n) . pq' = (((1 / 2) GeoSeq ) . n) * (pmet1 . pq') & f . pq' = (((1 / 2) GeoSeq ) . n) * (pmet1 . pq') ) by A23, A24, A25, A26, VALUED_1:def 5;
hence (GeoF' . n) . pq' = f . pq' ; :: thesis:

end;

take f ; :: thesis:

now

let pq' be Point of [:T,T:]; :: thesis:
reconsider pq = pq' as Element of [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
( (GeoF' . n) . pq' = (GeoF # pq) . n & (GeoF # pq) . n >= 0 ) by A11, SEQFUNC:def 11;
hence f . pq' >= 0 by A23, A26, A27; :: thesis:

end;

hence ( GeoF' . n = f & f is continuous & ( for pq' being Point of [:T,T:] holds f . pq' >= 0 ) ) by A23, A24, A26, A27, PARTFUN1:34, TOPREAL6:83; :: thesis:

end;

A28: ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for pq' being Point of [:T,T:] holds (GeoF' # pq') . n <= seq . n ) )

proof

take s (#) ((1 / 2) GeoSeq ) ; :: thesis:
thus s (#) ((1 / 2) GeoSeq ) is summable by A15, SERIES_1:13; :: thesis:

now

let n be Element of NAT ; :: thesis:
let pq' be Point of [:T,T:]; :: thesis:
reconsider pq = pq' as Element of [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
(GeoF' # pq') . n = (GeoF # pq) . n by A19;
hence (GeoF' # pq') . n <= (s (#) ((1 / 2) GeoSeq )) . n by A11; :: thesis:

end;

hence for n being Element of NAT
for pq' being Point of [:T,T:] holds (GeoF' # pq') . n <= (s (#) ((1 / 2) GeoSeq )) . n ; :: thesis:

end;

now

let pmet1' be RealMap of [:T,T:]; :: thesis:
assume A29: pmet = pmet1' ; :: thesis:
for pq' being Point of [:T,T:] holds pmet1' . pq' = Sum (GeoF' # pq')

proof

let pq' be Point of [:T,T:]; :: thesis:
reconsider pq = pq' as Element of [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
( pmet . pq = Sum (GeoF # pq) & GeoF # pq = GeoF' # pq' ) by A17, A19;
hence pmet1' . pq' = Sum (GeoF' # pq') by A29; :: thesis:

end;

hence pmet1' is continuous by A22, A28, Th14; :: thesis:

end;

hence ( pmet is_a_pseudometric_of the carrier of T & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) ) by A4, A16, A17, Th11; :: thesis: