let T be non empty TopSpace; :: thesis: ( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
thus ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is metrizable ) :: thesis: ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) )

proof

assume that
A1: T is regular and
A2: T is T_1 and
A3: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ; :: thesis: T is metrizable
consider Bn being FamilySequence of T such that
A4: Bn is Basis_sigma_locally_finite by A3;
A5: ( Bn is sigma_locally_finite & Union Bn is Basis of T ) by A4, NAGATA_1:def 6;
set cT = the carrier of T;
set bcT = bool the carrier of T;
set cTT = the carrier of [:T,T:];
set Fun = Funcs the carrier of [:T,T:],REAL ;
defpred S₁[ set , set , RealMap of [:T,T:]] means ex pmet being Function of [:the carrier of T,the carrier of T:],REAL st
( $3 = pmet & $3 is continuous & pmet is_a_pseudometric_of the carrier of T & ( for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . $2 & B in Bn . $1 & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) ) );
A6: for n, m being Element of NAT ex pmet' being RealMap of [:T,T:] st S₁[n,m,pmet']

proof

let n, m be Element of NAT ; :: thesis: ex pmet' being RealMap of [:T,T:] st S₁[n,m,pmet']
A7: ( Bn . n is locally_finite & Bn . m is locally_finite ) by A5, NAGATA_1:def 3;
deffunc H₁( set ) -> set = union { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= $1 ) } ;
A8: for A being set st A in bool the carrier of T holds
H₁(A) in bool the carrier of T

proof

let A be set ; :: thesis: ( A in bool the carrier of T implies H₁(A) in bool the carrier of T )
assume A in bool the carrier of T ; :: thesis: H₁(A) in bool the carrier of T
set Um = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ;

now

let uv be set ; :: thesis: ( uv in H₁(A) implies uv in the carrier of T )
assume A9: uv in H₁(A) ; :: thesis: uv in the carrier of T
consider v being set such that
A10: ( uv in v & v in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ) by A9, TARSKI:def 4;
consider B being Subset of T such that
A11: ( v = B & B in Bn . m & Cl B c= A ) by A10;
thus uv in the carrier of T by A10, A11; :: thesis: verum

end;

then H₁(A) c= the carrier of T by TARSKI:def 3;
hence H₁(A) in bool the carrier of T ; :: thesis: verum

end;

consider Vm being Function of (bool the carrier of T),(bool the carrier of T) such that
A12: for A being set st A in bool the carrier of T holds
Vm . A = H₁(A) from FUNCT_2:sch 2(A8);
A13: for A being Subset of T holds Cl (Vm . A) c= A

proof

let A be Subset of T; :: thesis: Cl (Vm . A) c= A
set VmA = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ;
{ Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } c= bool the carrier of T

proof

let B be set ; :: according to TARSKI:def 3 :: thesis: ( not B in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } or B in bool the carrier of T )
assume B in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ; :: thesis: B in bool the carrier of T
then ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) ;
hence B in bool the carrier of T ; :: thesis: verum

end;

then reconsider VmA = { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } as Subset-Family of T ;
VmA c= Bn . m

proof

let B be set ; :: according to TARSKI:def 3 :: thesis: ( not B in VmA or B in Bn . m )
assume B in VmA ; :: thesis: B in Bn . m
then ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) ;
hence B in Bn . m ; :: thesis: verum

end;

then A14: Cl (union VmA) = union (clf VmA) by A7, PCOMPS_1:12, PCOMPS_1:23;
union (clf VmA) c= A

proof

let ClBu be set ; :: according to TARSKI:def 3 :: thesis: ( not ClBu in union (clf VmA) or ClBu in A )
assume ClBu in union (clf VmA) ; :: thesis: ClBu in A
then consider ClB being set such that
A15: ( ClBu in ClB & ClB in clf VmA ) by TARSKI:def 4;
reconsider ClB = ClB as Subset of T by A15;
consider B being Subset of T such that
A16: ( Cl B = ClB & B in VmA ) by A15, PCOMPS_1:def 3;
ex C being Subset of T st
( B = C & C in Bn . m & Cl C c= A ) by A16;
hence ClBu in A by A15, A16; :: thesis: verum

end;

hence Cl (Vm . A) c= A by A12, A14; :: thesis: verum

end;

defpred S₂[ set , set ] means ex F being RealMap of T ex S being Subset of T st
( S = $1 & F = $2 & F is continuous & ( for p being Point of T holds
( 0 <= F . p & F . p <= 1 & ( p in S ` implies F . p = 0 ) & ( p in Cl (Vm . S) implies F . p = 1 ) ) ) );
set Bnn = Bn . n;
A17: for A being set st A in Bn . n holds
ex f being set st
( f in Funcs the carrier of T,REAL & S₂[A,f] )

proof

let A be set ; :: thesis: ( A in Bn . n implies ex f being set st
( f in Funcs the carrier of T,REAL & S₂[A,f] ) )
assume A in Bn . n ; :: thesis: ex f being set st
( f in Funcs the carrier of T,REAL & S₂[A,f] )
then ( A in Union Bn & Union Bn c= the topology of T ) by A5, CANTOR_1:def 2, PROB_1:25;
then reconsider A = A as open Subset of T by PRE_TOPC:def 5;
( Cl (Vm . A) c= A & A ` misses A ) by A13, XBOOLE_1:79;
then ( A ` misses Cl (Vm . A) & T is normal ) by A1, A2, A4, NAGATA_1:20, XBOOLE_1:63;
then consider f being Function of T,R^1 such that
A18: ( f is continuous & ( for p being Point of T holds
( 0 <= f . p & f . p <= 1 & ( p in A ` implies f . p = 0 ) & ( p in Cl (Vm . A) implies f . p = 1 ) ) ) ) by URYSOHN3:23;
reconsider f' = f as RealMap of T by TOPMETR:24;
A19: ex F being RealMap of T ex S being Subset of T st
( S = A & F = f' & F is continuous & ( for p being Point of T holds
( 0 <= F . p & F . p <= 1 & ( p in S ` implies F . p = 0 ) & ( p in Cl (Vm . S) implies F . p = 1 ) ) ) )

proof

take f' ; :: thesis: ex S being Subset of T st
( S = A & f' = f' & f' is continuous & ( for p being Point of T holds
( 0 <= f' . p & f' . p <= 1 & ( p in S ` implies f' . p = 0 ) & ( p in Cl (Vm . S) implies f' . p = 1 ) ) ) )
take A ; :: thesis: ( A = A & f' = f' & f' is continuous & ( for p being Point of T holds
( 0 <= f' . p & f' . p <= 1 & ( p in A ` implies f' . p = 0 ) & ( p in Cl (Vm . A) implies f' . p = 1 ) ) ) )
thus ( A = A & f' = f' & f' is continuous & ( for p being Point of T holds
( 0 <= f' . p & f' . p <= 1 & ( p in A ` implies f' . p = 0 ) & ( p in Cl (Vm . A) implies f' . p = 1 ) ) ) ) by A18, TOPREAL6:83; :: thesis: verum

end;

f' in Funcs the carrier of T,REAL by FUNCT_2:11;
hence ex f being set st
( f in Funcs the carrier of T,REAL & S₂[A,f] ) by A19; :: thesis: verum

end;

consider Fn being Function of (Bn . n),(Funcs the carrier of T,REAL ) such that
A20: for A being set st A in Bn . n holds
S₂[A,Fn . A] from FUNCT_2:sch 1(A17);
deffunc H₂( Subset of T) -> set = { Q where Q is Subset of T : ( Q in Bn . n & Q meets $1 ) } ;
defpred S₃[ set , Subset of T] means ( $1 in $2 & $2 is open & H₂($2) is finite );
A21: for p being Element of the carrier of T ex A being Element of bool the carrier of T st S₃[p,A] by A7, PCOMPS_1:def 2;
consider Sx being Function of the carrier of T,(bool the carrier of T) such that
A22: for p being Element of the carrier of T holds S₃[p,Sx . p] from FUNCT_2:sch 3(A21);
deffunc H₃( Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & A in H₂(Sx . $1) ) } ;
A23: for p being Point of T holds H₃(p) is finite

proof

let p be Point of T; :: thesis: H₃(p) is finite
deffunc H₄( Subset of T) -> set = Fn . $1;
set SFxx = { H₄(A) where A is Subset of T : A in H₂(Sx . p) } ;
A24: H₂(Sx . p) is finite by A22;
A25: { H₄(A) where A is Subset of T : A in H₂(Sx . p) } is finite from FRAENKEL:sch 21(A24);
H₃(p) c= { H₄(A) where A is Subset of T : A in H₂(Sx . p) }

proof

let FA be set ; :: according to TARSKI:def 3 :: thesis: ( not FA in H₃(p) or FA in { H₄(A) where A is Subset of T : A in H₂(Sx . p) } )
assume FA in H₃(p) ; :: thesis: FA in { H₄(A) where A is Subset of T : A in H₂(Sx . p) }
then ex A being Subset of T st
( FA = Fn . A & A in Bn . n & A in H₂(Sx . p) ) ;
hence FA in { H₄(A) where A is Subset of T : A in H₂(Sx . p) } ; :: thesis: verum

end;

hence H₃(p) is finite by A25; :: thesis: verum

end;

defpred S₄[ RealMap of T, Function] means for p, q being Point of T holds $2 . p,q = abs (($1 . p) - ($1 . q));
A26: for f being Element of Funcs the carrier of T,REAL ex fxy being Element of Funcs the carrier of [:T,T:],REAL st S₄[f,fxy]

proof

let f be Element of Funcs the carrier of T,REAL ; :: thesis: ex fxy being Element of Funcs the carrier of [:T,T:],REAL st S₄[f,fxy]
defpred S₅[ Element of T, Element of T, set ] means $3 = abs ((f . $1) - (f . $2));
A27: for x, y being Element of the carrier of T ex r being Element of REAL st S₅[x,y,r] ;
consider Fd being Function of [:the carrier of T,the carrier of T:],REAL such that
A28: for x, y being Element of the carrier of T holds S₅[x,y,Fd . x,y] from BINOP_1:sch 3(A27);
[:the carrier of T,the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 5;
then ( Fd in Funcs the carrier of [:T,T:],REAL & S₄[f,Fd] ) by A28, FUNCT_2:11;
hence ex fxy being Element of Funcs the carrier of [:T,T:],REAL st S₄[f,fxy] ; :: thesis: verum

end;

consider Fdist being Function of (Funcs the carrier of T,REAL ),(Funcs the carrier of [:T,T:],REAL ) such that
A29: for fd being Element of Funcs the carrier of T,REAL holds S₄[fd,Fdist . fd] from FUNCT_2:sch 3(A26);
A30: for p being Point of T
for fd being Element of Funcs the carrier of T,REAL st fd in H₃(p) holds
( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )

proof

let p be Point of T; :: thesis: for fd being Element of Funcs the carrier of T,REAL st fd in H₃(p) holds
( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
let fd be Element of Funcs the carrier of T,REAL ; :: thesis: ( fd in H₃(p) implies ( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) )
assume fd in H₃(p) ; :: thesis: ( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
then consider A being Subset of T such that
A31: ( fd = Fn . A & A in Bn . n & A in H₂(Sx . p) ) ;
A32: S₂[A,Fn . A] by A20, A31;
A33: ( S₄[fd,Fdist . fd] & Fdist . fd in Funcs the carrier of [:T,T:],REAL ) by A29;
reconsider FD = Fdist . fd as RealMap of [:T,T:] by FUNCT_2:121;
FD is continuous by A31, A32, A33, NAGATA_1:21;
hence ( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) by A29; :: thesis: verum

end;

deffunc H₄( set ) -> set = { (Fdist . fd) where fd is RealMap of T : fd in $1 } ;
defpred S₅[ set , Function] means ( $2 is one-to-one & ex p, q being Point of T st
( [p,q] = $1 & rng $2 = H₄(H₃(p) \/ H₃(q)) ) );
A34: for p, q being Point of T holds
( H₄(H₃(p) \/ H₃(q)) is finite & H₄(H₃(p) \/ H₃(q)) c= Funcs the carrier of [:T,T:],REAL )

proof

let p, q be Point of T; :: thesis: ( H₄(H₃(p) \/ H₃(q)) is finite & H₄(H₃(p) \/ H₃(q)) c= Funcs the carrier of [:T,T:],REAL )
A35: H₄(H₃(p) \/ H₃(q)) c= Funcs the carrier of [:T,T:],REAL

proof

let FDm be set ; :: according to TARSKI:def 3 :: thesis: ( not FDm in H₄(H₃(p) \/ H₃(q)) or FDm in Funcs the carrier of [:T,T:],REAL )
assume FDm in H₄(H₃(p) \/ H₃(q)) ; :: thesis: FDm in Funcs the carrier of [:T,T:],REAL
then consider fd being RealMap of T such that
A36: ( FDm = Fdist . fd & fd in H₃(p) \/ H₃(q) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
hence FDm in Funcs the carrier of [:T,T:],REAL by A36, FUNCT_2:7; :: thesis: verum

end;

deffunc H₅( RealMap of T) -> set = Fdist . $1;
set RNG' = { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) } ;
( H₃(p) is finite & H₃(q) is finite ) by A23;
then A37: H₃(p) \/ H₃(q) is finite ;
A38: { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) } is finite from FRAENKEL:sch 21(A37);
H₄(H₃(p) \/ H₃(q)) c= { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) }

proof

let Fdistfd be set ; :: according to TARSKI:def 3 :: thesis: ( not Fdistfd in H₄(H₃(p) \/ H₃(q)) or Fdistfd in { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) } )
assume Fdistfd in H₄(H₃(p) \/ H₃(q)) ; :: thesis: Fdistfd in { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) }
then consider fd being RealMap of T such that
A39: ( Fdistfd = Fdist . fd & fd in H₃(p) \/ H₃(q) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
hence Fdistfd in { H₅(fd) where fd is Element of Funcs the carrier of T,REAL : fd in H₃(p) \/ H₃(q) } by A39; :: thesis: verum

end;

hence ( H₄(H₃(p) \/ H₃(q)) is finite & H₄(H₃(p) \/ H₃(q)) c= Funcs the carrier of [:T,T:],REAL ) by A35, A38; :: thesis: verum

end;

A40: for pq being Element of the carrier of [:T,T:] ex G being Element of (Funcs the carrier of [:T,T:],REAL ) * st S₅[pq,G]

proof

let pq be Element of the carrier of [:T,T:]; :: thesis: ex G being Element of (Funcs the carrier of [:T,T:],REAL ) * st S₅[pq,G]
pq in the carrier of [:T,T:] ;
then pq in [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then consider p, q being set such that
A41: ( p in the carrier of T & q in the carrier of T & pq = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A41;
H₄(H₃(p) \/ H₃(q)) is finite by A34;
then consider SF being FinSequence such that
A42: ( rng SF = H₄(H₃(p) \/ H₃(q)) & SF is one-to-one ) by FINSEQ_4:73;
rng SF c= Funcs the carrier of [:T,T:],REAL by A34, A42;
then reconsider SF = SF as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 4;
( SF in (Funcs the carrier of [:T,T:],REAL ) * & S₅[pq,SF] ) by A41, A42, FINSEQ_1:def 11;
hence ex G being Element of (Funcs the carrier of [:T,T:],REAL ) * st S₅[pq,G] ; :: thesis: verum

end;

consider SFdist being Function of the carrier of [:T,T:],((Funcs the carrier of [:T,T:],REAL ) * ) such that
A43: for pq being Element of the carrier of [:T,T:] holds S₅[pq,SFdist . pq] from FUNCT_2:sch 3(A40);
defpred S₆[ Element of Funcs the carrier of [:T,T:],REAL , Element of Funcs the carrier of [:T,T:],REAL , set ] means $1 + $2 = $3;
A44: for f, g being Element of Funcs the carrier of [:T,T:],REAL ex fg being Element of Funcs the carrier of [:T,T:],REAL st S₆[f,g,fg]

proof

let f, g be Element of Funcs the carrier of [:T,T:],REAL ; :: thesis: ex fg being Element of Funcs the carrier of [:T,T:],REAL st S₆[f,g,fg]
set f' = f;
set g' = g;
f + g in Funcs the carrier of [:T,T:],REAL by FUNCT_2:11;
hence ex fg being Element of Funcs the carrier of [:T,T:],REAL st S₆[f,g,fg] ; :: thesis: verum

end;

consider ADD being BinOp of (Funcs the carrier of [:T,T:],REAL ) such that
A45: for f, g being Element of Funcs the carrier of [:T,T:],REAL holds S₆[f,g,ADD . f,g] from BINOP_1:sch 3(A44);
A46: for f1, f2 being RealMap of [:T,T:] holds ADD . f1,f2 = f1 + f2

proof

let f1, f2 be RealMap of [:T,T:]; :: thesis: ADD . f1,f2 = f1 + f2
reconsider f1' = f1, f2' = f2 as Element of Funcs the carrier of [:T,T:],REAL by FUNCT_2:11;
ADD . f1',f2' = f1' + f2' by A45;
hence ADD . f1,f2 = f1 + f2 ; :: thesis: verum

end;

defpred S₇[ set , set ] means for FS being FinSequence of Funcs the carrier of [:T,T:],REAL st FS = SFdist . $1 holds
$2 = ADD "**" FS;
A47: for pq being set st pq in the carrier of [:T,T:] holds
ex S being set st
( S in Funcs the carrier of [:T,T:],REAL & S₇[pq,S] )

proof

let pq be set ; :: thesis: ( pq in the carrier of [:T,T:] implies ex S being set st
( S in Funcs the carrier of [:T,T:],REAL & S₇[pq,S] ) )
assume pq in the carrier of [:T,T:] ; :: thesis: ex S being set st
( S in Funcs the carrier of [:T,T:],REAL & S₇[pq,S] )
then SFdist . pq in (Funcs the carrier of [:T,T:],REAL ) * by FUNCT_2:7;
then reconsider SF = SFdist . pq as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
for FS being FinSequence of Funcs the carrier of [:T,T:],REAL st FS = SFdist . pq holds
ADD "**" FS = ADD "**" SF ;
hence ex S being set st
( S in Funcs the carrier of [:T,T:],REAL & S₇[pq,S] ) ; :: thesis: verum

end;

consider SumFdist being Function of the carrier of [:T,T:],(Funcs the carrier of [:T,T:],REAL ) such that
A48: for xy being set st xy in the carrier of [:T,T:] holds
S₇[xy,SumFdist . xy] from FUNCT_2:sch 1(A47);
A49: for pq' being Point of [:T,T:] holds SumFdist . pq' is continuous RealMap of [:T,T:]

proof

let pq' be Point of [:T,T:]; :: thesis: SumFdist . pq' is continuous RealMap of [:T,T:]
reconsider SF = SFdist . pq' as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
consider p, q being Point of T such that
A50: ( [p,q] = pq' & rng SF = H₄(H₃(p) \/ H₃(q)) ) by A43;
for n being Element of NAT st 0 <> n & n <= len SF holds
SF . n is continuous RealMap of [:T,T:]

proof

let n be Element of NAT ; :: thesis: ( 0 <> n & n <= len SF implies SF . n is continuous RealMap of [:T,T:] )
assume A51: ( 0 <> n & n <= len SF ) ; :: thesis: SF . n is continuous RealMap of [:T,T:]
then n >= 1 by NAT_1:14;
then n in dom SF by A51, FINSEQ_3:27;
then SF . n in H₄(H₃(p) \/ H₃(q)) by A50, FUNCT_1:def 5;
then consider fd being RealMap of T such that
A52: ( SF . n = Fdist . fd & fd in H₃(p) \/ H₃(q) ) ;
A53: fd in Funcs the carrier of T,REAL by FUNCT_2:11;
( fd in H₃(p) or fd in H₃(q) ) by A52, XBOOLE_0:def 3;
hence SF . n is continuous RealMap of [:T,T:] by A30, A52, A53; :: thesis: verum

end;

then ( ADD "**" SF is continuous RealMap of [:T,T:] & SF = SFdist . pq' ) by A46, NAGATA_1:25;
hence SumFdist . pq' is continuous RealMap of [:T,T:] by A48; :: thesis: verum

end;

reconsider SumFdist' = SumFdist as Function of the carrier of [:T,T:],(Funcs the carrier of [:T,T:],the carrier of R^1 ) by TOPMETR:24;
A54: for pq' being Point of [:T,T:] holds SumFdist' . pq' is continuous Function of [:T,T:],R^1

proof

let pq' be Point of [:T,T:]; :: thesis: SumFdist' . pq' is continuous Function of [:T,T:],R^1
reconsider SF = SumFdist . pq' as Function of [:T,T:],R^1 by A49, TOPMETR:24;
SumFdist . pq' is continuous RealMap of [:T,T:] by A49;
then SF is continuous by TOPREAL6:83;
hence SumFdist' . pq' is continuous Function of [:T,T:],R^1 ; :: thesis: verum

end;

defpred S₈[ set , set ] means for x, y being Element of T st $1 = [x,y] holds
$2 = [:(Sx . x),(Sx . y):];
A55: for pq' being set st pq' in the carrier of [:T,T:] holds
ex SS being set st
( SS in bool the carrier of [:T,T:] & S₈[pq',SS] )

proof

let pq' be set ; :: thesis: ( pq' in the carrier of [:T,T:] implies ex SS being set st
( SS in bool the carrier of [:T,T:] & S₈[pq',SS] ) )
assume pq' in the carrier of [:T,T:] ; :: thesis: ex SS being set st
( SS in bool the carrier of [:T,T:] & S₈[pq',SS] )
then pq' in [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then consider p, q being set such that
A56: ( p in the carrier of T & q in the carrier of T & pq' = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A56;

now

let p1, q1 be Point of T; :: thesis: ( pq' = [p1,q1] implies [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] )
assume pq' = [p1,q1] ; :: thesis: [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]
then ( p1 = p & q1 = q ) by A56, ZFMISC_1:33;
hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] ; :: thesis: verum

end;

hence ex SS being set st
( SS in bool the carrier of [:T,T:] & S₈[pq',SS] ) ; :: thesis: verum

end;

consider SS being Function of the carrier of [:T,T:],(bool the carrier of [:T,T:]) such that
A57: for pq being set st pq in the carrier of [:T,T:] holds
S₈[pq,SS . pq] from FUNCT_2:sch 1(A55);
A58: for pq' being Point of [:T,T:] holds
( pq' in SS . pq' & SS . pq' is open )

proof

let pq' be Point of [:T,T:]; :: thesis: ( pq' in SS . pq' & SS . pq' is open )
pq' in the carrier of [:T,T:] ;
then pq' in [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then consider p, q being set such that
A59: ( p in the carrier of T & q in the carrier of T & pq' = [p,q] ) by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A59;
( SS . pq' = [:(Sx . p),(Sx . q):] & p in Sx . p & q in Sx . q & Sx . p is open & Sx . q is open ) by A22, A57, A59;
hence ( pq' in SS . pq' & SS . pq' is open ) by A59, BORSUK_1:46, ZFMISC_1:def 2; :: thesis: verum

end;

A60: for pq being Element of the carrier of [:T,T:]
for map' being Element of Funcs the carrier of [:T,T:],REAL st map' is_a_unity_wrt ADD holds
map' . pq = 0

proof

let pq be Element of the carrier of [:T,T:]; :: thesis: for map' being Element of Funcs the carrier of [:T,T:],REAL st map' is_a_unity_wrt ADD holds
map' . pq = 0
let map' be Element of Funcs the carrier of [:T,T:],REAL ; :: thesis: ( map' is_a_unity_wrt ADD implies map' . pq = 0 )
assume map' is_a_unity_wrt ADD ; :: thesis: map' . pq = 0
then ADD . map',map' = map' by BINOP_1:11;
then (map' + map') . pq = map' . pq by A45;
then (map' . pq) + (map' . pq) = map' . pq by NAGATA_1:def 7;
hence map' . pq = 0 ; :: thesis: verum

end;

A61: for pq1, pq2 being Point of [:T,T:] holds
( ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) & ( for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ) )

proof

let pq1, pq2 be Point of [:T,T:]; :: thesis: ( ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) & ( for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ) )
deffunc H₅( Element of T, Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & ( for FnA being RealMap of T holds
( not Fn . A = FnA or FnA . $1 > 0 or FnA . $2 > 0 ) ) ) } ;
A62: for p, q, p1, q1 being Point of T st [p,q] in SS . [p1,q1] holds
H₅(p,q) c= H₃(p1) \/ H₃(q1)

proof

let p, q, p1, q1 be Point of T; :: thesis: ( [p,q] in SS . [p1,q1] implies H₅(p,q) c= H₃(p1) \/ H₃(q1) )
assume A63: [p,q] in SS . [p1,q1] ; :: thesis: H₅(p,q) c= H₃(p1) \/ H₃(q1)
let no0 be set ; :: according to TARSKI:def 3 :: thesis: ( not no0 in H₅(p,q) or no0 in H₃(p1) \/ H₃(q1) )
assume no0 in H₅(p,q) ; :: thesis: no0 in H₃(p1) \/ H₃(q1)
then consider A being Subset of T such that
A64: ( no0 = Fn . A & A in Bn . n & ( for FnA being RealMap of T holds
( not Fn . A = FnA or FnA . p > 0 or FnA . q > 0 ) ) ) ;
Fn . A in Funcs the carrier of T,REAL by A64, FUNCT_2:7;
then reconsider FnA = Fn . A as RealMap of T by FUNCT_2:121;
reconsider pq1 = [p1,q1] as Element of the carrier of [:T,T:] by BORSUK_1:def 5;
A65: ( FnA . p > 0 or FnA . q > 0 ) by A64;
S₂[A,Fn . A] by A20, A64;
then ( ( not p in the carrier of T \ A or not q in the carrier of T \ A ) & [:(Sx . p1),(Sx . q1):] = SS . pq1 ) by A57, A65;
then ( ( p in A or q in A ) & p in Sx . p1 & q in Sx . q1 ) by A63, XBOOLE_0:def 5, ZFMISC_1:106;
then ( A meets Sx . p1 or A meets Sx . q1 ) by XBOOLE_0:3;
then ( A in H₂(Sx . p1) or A in H₂(Sx . q1) ) by A64;
then ( FnA in H₃(p1) or FnA in H₃(q1) ) by A64;
hence no0 in H₃(p1) \/ H₃(q1) by A64, XBOOLE_0:def 3; :: thesis: verum

end;

A66: for f being FinSequence of Funcs the carrier of [:T,T:],REAL
for p, q, p1, q1 being Point of T st rng f = H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) holds
(ADD "**" f) . [p,q] = 0

proof

let f be FinSequence of Funcs the carrier of [:T,T:],REAL ; :: thesis: for p, q, p1, q1 being Point of T st rng f = H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) holds
(ADD "**" f) . [p,q] = 0
let p, q, p1, q1 be Point of T; :: thesis: ( rng f = H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) implies (ADD "**" f) . [p,q] = 0 )
assume A67: rng f = H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) ; :: thesis: (ADD "**" f) . [p,q] = 0
reconsider pq = [p,q] as Element of the carrier of [:T,T:] by BORSUK_1:def 5;

now

per cases ( len f = 0 or len f <> 0 ) ;

suppose A68: len f = 0 ; :: thesis: (ADD "**" f) . pq = 0

ADD is having_a_unity by A46, NAGATA_1:23;
then ( ADD "**" f = the_unity_wrt ADD & ex f being Element of Funcs the carrier of [:T,T:],REAL st f is_a_unity_wrt ADD ) by A68, FINSOP_1:def 1, SETWISEO:def 2;
then ADD "**" f is_a_unity_wrt ADD by BINOP_1:def 8;
hence (ADD "**" f) . pq = 0 by A60; :: thesis: verum

end;

suppose A69: len f <> 0 ; :: thesis: (ADD "**" f) . pq = 0

then len f >= 1 by NAT_1:14;
then consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A70: ( F . 1 = f . 1 & ( for n being Element of NAT st 0 <> n & n < len f holds
F . (n + 1) = ADD . (F . n),(f . (n + 1)) ) & ADD "**" f = F . (len f) ) by FINSOP_1:def 1;
defpred S₉[ Element of NAT ] means ( $1 <> 0 & $1 <= len f implies (F . $1) . pq = 0 );
A71: S₉[ 0 ] ;
A72: for k being Element of NAT st S₉[k] holds
S₉[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume A73: S₉[k] ; :: thesis: S₉[k + 1]
assume A74: ( k + 1 <> 0 & k + 1 <= len f ) ; :: thesis: (F . (k + 1)) . pq = 0
then A75: ( k + 1 <= len f & k < len f & k + 1 >= 1 ) by NAT_1:13, NAT_1:14;
then k + 1 in dom f by FINSEQ_3:27;
then f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) by A67, FUNCT_1:def 5;
then A76: ( f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) & not f . (k + 1) in H₄(H₅(p,q)) ) by XBOOLE_0:def 5;
then consider fd being RealMap of T such that
A77: ( Fdist . fd = f . (k + 1) & fd in H₃(p1) \/ H₃(q1) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, fk1 = f . (k + 1) as RealMap of [:T,T:] by A77, FUNCT_2:7, FUNCT_2:121;
( fd . p = 0 & fd . q = 0 )

proof

assume A78: ( fd . p <> 0 or fd . q <> 0 ) ; :: thesis: contradiction

per cases ( fd in H₃(p1) or fd in H₃(q1) ) by A77, XBOOLE_0:def 3;

suppose fd in H₃(p1) ; :: thesis: contradiction

then consider A being Subset of T such that
A79: ( fd = Fn . A & A in Bn . n & A in H₂(Sx . p1) ) ;
not fd in H₅(p,q) by A76, A77;
then consider FnA being RealMap of T such that
A80: ( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A79;
S₂[A,Fn . A] by A20, A79;
hence contradiction by A78, A79, A80; :: thesis: verum

end;

suppose fd in H₃(q1) ; :: thesis: contradiction

then consider A being Subset of T such that
A81: ( fd = Fn . A & A in Bn . n & A in H₂(Sx . q1) ) ;
not fd in H₅(p,q) by A76, A77;
then consider FnA being RealMap of T such that
A82: ( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A81;
S₂[A,Fn . A] by A20, A81;
hence contradiction by A78, A81, A82; :: thesis: verum

end;

end;

end;

then ( (fd . p) - (fd . q) = 0 & fd in Funcs the carrier of T,REAL ) by FUNCT_2:11;
then A83: ( abs ((fd . p) - (fd . q)) = 0 & Fdistfd . p,q = abs ((fd . p) - (fd . q)) ) by A29, ABSVALUE:7;

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: (F . (k + 1)) . pq = 0

hence (F . (k + 1)) . pq = 0 by A70, A77, A83; :: thesis: verum

end;

suppose k > 0 ; :: thesis: (F . (k + 1)) . pq = 0

then ( Fk1 = ADD . Fk,fk1 & k > 0 ) by A70, A75;
then ( Fk1 = Fk + fk1 & Fk . pq = 0 ) by A46, A73, A74, NAT_1:13;
then Fk1 . pq = 0 + (fk1 . pq) by NAGATA_1:def 7;
hence (F . (k + 1)) . pq = 0 by A77, A83; :: thesis: verum

end;

end;

end;

for n being Element of NAT holds S₉[n] from NAT_1:sch 1(A71, A72);
hence (ADD "**" f) . pq = 0 by A69, A70; :: thesis: verum

end;

end;

end;

hence (ADD "**" f) . [p,q] = 0 ; :: thesis: verum

end;

reconsider S1 = SFdist . pq1, S2 = SFdist . pq2 as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
consider p1, q1 being Point of T such that
A84: ( [p1,q1] = pq1 & rng S1 = H₄(H₃(p1) \/ H₃(q1)) ) by A43;
consider p2, q2 being Point of T such that
A85: ( [p2,q2] = pq2 & rng S2 = H₄(H₃(p2) \/ H₃(q2)) ) by A43;
A86: H₄(H₅(p1,q1)) c= H₄(H₃(p1) \/ H₃(q1))

proof

let FD be set ; :: according to TARSKI:def 3 :: thesis: ( not FD in H₄(H₅(p1,q1)) or FD in H₄(H₃(p1) \/ H₃(q1)) )
assume A87: FD in H₄(H₅(p1,q1)) ; :: thesis: FD in H₄(H₃(p1) \/ H₃(q1))
consider fd being RealMap of T such that
A88: ( FD = Fdist . fd & fd in H₅(p1,q1) ) by A87;
( p1 in Sx . p1 & q1 in Sx . q1 ) by A22;
then [p1,q1] in [:(Sx . p1),(Sx . q1):] by ZFMISC_1:106;
then [p1,q1] in SS . [p1,q1] by A57;
then H₅(p1,q1) c= H₃(p1) \/ H₃(q1) by A62;
hence FD in H₄(H₃(p1) \/ H₃(q1)) by A88; :: thesis: verum

end;

reconsider S1 = SFdist . pq1, S2 = SFdist . pq2 as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
H₄(H₃(p1) \/ H₃(q1)) is finite by A34;
then A89: H₄(H₅(p1,q1)) is finite by A86;
then consider No being FinSequence such that
A90: ( rng No = H₄(H₅(p1,q1)) & No is one-to-one ) by FINSEQ_4:73;
H₄(H₃(p1) \/ H₃(q1)) c= Funcs the carrier of [:T,T:],REAL by A34;
then A91: H₄(H₅(p1,q1)) c= Funcs the carrier of [:T,T:],REAL by A86, XBOOLE_1:1;
then reconsider No = No as FinSequence of Funcs the carrier of [:T,T:],REAL by A90, FINSEQ_1:def 4;
A92: ( ADD is having_a_unity & ADD is commutative & ADD is associative ) by A46, NAGATA_1:23;
( rng No c= rng S1 & S1 is one-to-one ) by A43, A84, A86, A90;
then consider S1No being FinSequence of Funcs the carrier of [:T,T:],REAL such that
A93: ( S1No is one-to-one & rng S1No = (rng S1) \ (rng No) & ADD "**" S1 = ADD . (ADD "**" No),(ADD "**" S1No) ) by A90, A92, Th18;
set RNiS2 = H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2));
H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) is finite by A89;
then consider NoiS2 being FinSequence such that
A94: ( rng NoiS2 = H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) & NoiS2 is one-to-one ) by FINSEQ_4:73;
H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) c= H₄(H₅(p1,q1)) by XBOOLE_1:17;
then H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) c= Funcs the carrier of [:T,T:],REAL by A91, XBOOLE_1:1;
then reconsider NoiS2 = NoiS2 as FinSequence of Funcs the carrier of [:T,T:],REAL by A94, FINSEQ_1:def 4;
( rng NoiS2 c= rng No & No is one-to-one ) by A90, A94, XBOOLE_1:17;
then consider NoNoiS2 being FinSequence of Funcs the carrier of [:T,T:],REAL such that
A95: ( NoNoiS2 is one-to-one & rng NoNoiS2 = (rng No) \ (rng NoiS2) & ADD "**" No = ADD . (ADD "**" NoiS2),(ADD "**" NoNoiS2) ) by A92, A94, Th18;
( rng NoiS2 c= rng S2 & S2 is one-to-one ) by A43, A85, A94, XBOOLE_1:17;
then consider S2No being FinSequence of Funcs the carrier of [:T,T:],REAL such that
A96: ( S2No is one-to-one & rng S2No = (rng S2) \ (rng NoiS2) & ADD "**" S2 = ADD . (ADD "**" NoiS2),(ADD "**" S2No) ) by A92, A94, Th18;
reconsider ANoNoiS2 = ADD "**" NoNoiS2, ANo = ADD "**" No, AS1No = ADD "**" S1No, AS2No = ADD "**" S2No, ANoiS2 = ADD "**" NoiS2, AS1 = ADD "**" S1, AS2 = ADD "**" S2 as RealMap of [:T,T:] by FUNCT_2:121;
A97: ANoNoiS2 . p1,q1 >= 0

proof

set N = NoNoiS2;

per cases ( len NoNoiS2 = 0 or len NoNoiS2 <> 0 ) ;

suppose A98: len NoNoiS2 = 0 ; :: thesis: ANoNoiS2 . p1,q1 >= 0

ADD is having_a_unity by A46, NAGATA_1:23;
then ( ADD "**" NoNoiS2 = the_unity_wrt ADD & ex f being Element of Funcs the carrier of [:T,T:],REAL st f is_a_unity_wrt ADD ) by A98, FINSOP_1:def 1, SETWISEO:def 2;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by BINOP_1:def 8;
hence ANoNoiS2 . p1,q1 >= 0 by A60, A84; :: thesis: verum

end;

suppose A99: len NoNoiS2 <> 0 ; :: thesis: ANoNoiS2 . p1,q1 >= 0

then len NoNoiS2 >= 1 by NAT_1:14;
then consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A100: ( F . 1 = NoNoiS2 . 1 & ( for n being Element of NAT st 0 <> n & n < len NoNoiS2 holds
F . (n + 1) = ADD . (F . n),(NoNoiS2 . (n + 1)) ) & ADD "**" NoNoiS2 = F . (len NoNoiS2) ) by FINSOP_1:def 1;
defpred S₉[ Element of NAT ] means ( $1 <> 0 & $1 <= len NoNoiS2 implies for Fn being RealMap of [:T,T:] st Fn = F . $1 holds
Fn . p1,q1 >= 0 );
A101: S₉[ 0 ] ;
A102: for k being Element of NAT st S₉[k] holds
S₉[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume A103: S₉[k] ; :: thesis: S₉[k + 1]
assume A104: ( k + 1 <> 0 & k + 1 <= len NoNoiS2 ) ; :: thesis: for Fn being RealMap of [:T,T:] st Fn = F . (k + 1) holds
Fn . p1,q1 >= 0
then A105: ( k + 1 <= len NoNoiS2 & k < len NoNoiS2 & k + 1 >= 1 ) by NAT_1:13, NAT_1:14;
then k + 1 in dom NoNoiS2 by FINSEQ_3:27;
then NoNoiS2 . (k + 1) in (rng No) \ (rng NoiS2) by A95, FUNCT_1:def 5;
then NoNoiS2 . (k + 1) in H₄(H₅(p1,q1)) by A90, XBOOLE_0:def 5;
then consider fd being RealMap of T such that
A106: ( Fdist . fd = NoNoiS2 . (k + 1) & fd in H₅(p1,q1) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, Nk1 = NoNoiS2 . (k + 1) as RealMap of [:T,T:] by A106, FUNCT_2:7, FUNCT_2:121;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then A107: ( abs ((fd . p1) - (fd . q1)) >= 0 & Fdistfd . p1,q1 = abs ((fd . p1) - (fd . q1)) ) by A29, COMPLEX1:132;

A108: now

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: Fk1 . p1,q1 >= 0

hence Fk1 . p1,q1 >= 0 by A100, A106, A107; :: thesis: verum

end;

suppose k > 0 ; :: thesis: Fk1 . p1,q1 >= 0

then ( Fk1 = ADD . Fk,Nk1 & k > 0 ) by A100, A105;
then ( Fk1 = Fk + Nk1 & Fk . p1,q1 >= 0 & Nk1 . p1,q1 >= 0 ) by A46, A103, A104, A106, A107, NAT_1:13;
then ( 0 + 0 <= (Fk . p1,q1) + (Nk1 . p1,q1) & (Fk . p1,q1) + (Nk1 . p1,q1) = Fk1 . p1,q1 ) by A84, NAGATA_1:def 7;
hence Fk1 . p1,q1 >= 0 ; :: thesis: verum

end;

end;

end;

let Fn be RealMap of [:T,T:]; :: thesis: ( Fn = F . (k + 1) implies Fn . p1,q1 >= 0 )
assume Fn = F . (k + 1) ; :: thesis: Fn . p1,q1 >= 0
hence Fn . p1,q1 >= 0 by A108; :: thesis: verum

end;

for n being Element of NAT holds S₉[n] from NAT_1:sch 1(A101, A102);
hence ANoNoiS2 . p1,q1 >= 0 by A99, A100; :: thesis: verum

end;

end;

end;

( AS1 = ANo + AS1No & ANo = ANoiS2 + ANoNoiS2 & AS2 = ANoiS2 + AS2No & rng S2No = H₄(H₃(p2) \/ H₃(q2)) \ H₄(H₅(p1,q1)) ) by A46, A85, A93, A94, A95, A96, XBOOLE_1:47;
then A109: ( AS1 . pq1 = (ANo . pq1) + (AS1No . pq1) & ANo . pq1 = (ANoiS2 . pq1) + (ANoNoiS2 . pq1) & AS2 . pq1 = (ANoiS2 . pq1) + (AS2No . pq1) & AS1No . pq1 = 0 & AS2No . pq1 = 0 ) by A66, A84, A90, A93, NAGATA_1:def 7;
thus ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) :: thesis: for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1

proof

assume A110: pq1 in SS . pq2 ; :: thesis: (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1

now

let FD be set ; :: thesis: ( FD in H₄(H₅(p1,q1)) implies FD in H₄(H₃(p2) \/ H₃(q2)) )
assume FD in H₄(H₅(p1,q1)) ; :: thesis: FD in H₄(H₃(p2) \/ H₃(q2))
then consider fd being RealMap of T such that
A111: ( FD = Fdist . fd & fd in H₅(p1,q1) ) ;
H₅(p1,q1) c= H₃(p2) \/ H₃(q2) by A62, A84, A85, A110;
hence FD in H₄(H₃(p2) \/ H₃(q2)) by A111; :: thesis: verum

end;

then H₄(H₅(p1,q1)) c= H₄(H₃(p2) \/ H₃(q2)) by TARSKI:def 3;
then ( H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) = H₄(H₅(p1,q1)) & rng NoNoiS2 = H₄(H₅(p1,q1)) \ (H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2))) ) by A90, A94, A95, XBOOLE_1:28;
then rng NoNoiS2 = {} by XBOOLE_1:37;
then NoNoiS2 = {} by RELAT_1:64;
then ( len NoNoiS2 = 0 & ADD is having_a_unity ) by A46, NAGATA_1:23;
then ( ADD "**" NoNoiS2 = the_unity_wrt ADD & ex f being Element of Funcs the carrier of [:T,T:],REAL st f is_a_unity_wrt ADD ) by FINSOP_1:def 1, SETWISEO:def 2;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by BINOP_1:def 8;
then ( AS1 . pq1 = AS2 . pq1 & SumFdist . pq1 = AS1 ) by A48, A60, A109;
hence (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 by A48; :: thesis: verum

end;

now

let SumFdist1, SumFdist2 be RealMap of [:T,T:]; :: thesis: ( SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 implies SumFdist1 . pq1 >= SumFdist2 . pq1 )
assume A112: ( SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 ) ; :: thesis: SumFdist1 . pq1 >= SumFdist2 . pq1
then ( AS2 . p1,q1 <= AS1 . p1,q1 & SumFdist2 = AS2 ) by A48, A84, A97, A109, XREAL_1:9;
hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A48, A84, A112; :: thesis: verum

end;

hence for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds
SumFdist1 . pq1 >= SumFdist2 . pq1 ; :: thesis: verum

end;

the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then reconsider SumFTS = SumFdist' Toler as Function of [:the carrier of T,the carrier of T:],REAL by TOPMETR:24;
reconsider SumFTS' = SumFdist' Toler as RealMap of [:T,T:] by TOPMETR:24;
for p, q being Point of [:T,T:] st p in SS . q holds
(SumFdist' . p) . p = (SumFdist' . q) . p by A61;
then SumFdist' Toler is continuous by A54, A58, NAGATA_1:26;
then A113: SumFTS' is continuous by TOPREAL6:83;

now

let p, q, r be Point of T; :: thesis: ( SumFTS . p,p = 0 & SumFTS . p,r <= (SumFTS . p,q) + (SumFTS . r,q) )
thus SumFTS . p,p = 0 :: thesis: SumFTS . p,r <= (SumFTS . p,q) + (SumFTS . r,q)

proof

reconsider pp = [p,p] as Point of [:T,T:] by BORSUK_1:def 5;
reconsider SF = SFdist . pp as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;

now

per cases ( len SF = 0 or len SF <> 0 ) ;

suppose A114: len SF = 0 ; :: thesis: (ADD "**" SF) . pp = 0

ADD is having_a_unity by A46, NAGATA_1:23;
then ( ADD "**" SF = the_unity_wrt ADD & ex f being Element of Funcs the carrier of [:T,T:],REAL st f is_a_unity_wrt ADD ) by A114, FINSOP_1:def 1, SETWISEO:def 2;
then ADD "**" SF is_a_unity_wrt ADD by BINOP_1:def 8;
hence (ADD "**" SF) . pp = 0 by A60; :: thesis: verum

end;

suppose A115: len SF <> 0 ; :: thesis: (ADD "**" SF) . pp = 0

then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A116: ( F . 1 = SF . 1 & ( for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . (F . n),(SF . (n + 1)) ) & ADD "**" SF = F . (len SF) ) by FINSOP_1:def 1;
defpred S₉[ Element of NAT ] means ( $1 <> 0 & $1 <= len SF implies (F . $1) . pp = 0 );
A117: S₉[ 0 ] ;
A118: for k being Element of NAT st S₉[k] holds
S₉[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume A119: S₉[k] ; :: thesis: S₉[k + 1]
assume A120: ( k + 1 <> 0 & k + 1 <= len SF ) ; :: thesis: (F . (k + 1)) . pp = 0
then A121: ( k + 1 <= len SF & k < len SF & k + 1 >= 1 ) by NAT_1:13, NAT_1:14;
then A122: k + 1 in dom SF by FINSEQ_3:27;
consider x, y being Point of T such that
A123: ( [x,y] = pp & rng SF = H₄(H₃(x) \/ H₃(y)) ) by A43;
SF . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A122, A123, FUNCT_1:def 5;
then consider fd being RealMap of T such that
A124: ( Fdist . fd = SF . (k + 1) & fd in H₃(x) \/ H₃(y) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SF . (k + 1) as RealMap of [:T,T:] by A124, FUNCT_2:7, FUNCT_2:121;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then A125: ( abs ((fd . p) - (fd . p)) = 0 & Fdistfd . p,p = abs ((fd . p) - (fd . p)) ) by A29, ABSVALUE:7;

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: (F . (k + 1)) . pp = 0

hence (F . (k + 1)) . pp = 0 by A116, A124, A125; :: thesis: verum

end;

suppose k > 0 ; :: thesis: (F . (k + 1)) . pp = 0

then ( Fk1 = ADD . Fk,SFk1 & k > 0 ) by A116, A121;
then ( Fk1 = Fk + SFk1 & Fk . pp = 0 ) by A46, A119, A120, NAT_1:13;
then Fk1 . pp = 0 + (SFk1 . pp) by NAGATA_1:def 7;
hence (F . (k + 1)) . pp = 0 by A124, A125; :: thesis: verum

end;

end;

end;

for n being Element of NAT holds S₉[n] from NAT_1:sch 1(A117, A118);
hence (ADD "**" SF) . pp = 0 by A115, A116; :: thesis: verum

end;

end;

end;

then ( (ADD "**" SF) . pp = 0 & SumFdist . pp = ADD "**" SF ) by A48;
hence SumFTS . p,p = 0 by NAGATA_1:def 8; :: thesis: verum

end;

thus SumFTS . p,r <= (SumFTS . p,q) + (SumFTS . r,q) :: thesis: verum

proof

reconsider pr = [p,r], pq = [p,q], rq = [r,q] as Point of [:T,T:] by BORSUK_1:def 5;
reconsider SFpr = SFdist . pr as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
reconsider ASFpr = ADD "**" SFpr as RealMap of [:T,T:] by FUNCT_2:121;
reconsider SumFpr = SumFdist . pr, SumFpq = SumFdist . pq, SumFrq = SumFdist . rq as RealMap of [:T,T:] by FUNCT_2:121;

now

per cases ( len SFpr = 0 or len SFpr <> 0 ) ;

suppose A126: len SFpr = 0 ; :: thesis: ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq)

ADD is having_a_unity by A46, NAGATA_1:23;
then ( ADD "**" SFpr = the_unity_wrt ADD & ex f being Element of Funcs the carrier of [:T,T:],REAL st f is_a_unity_wrt ADD ) by A126, FINSOP_1:def 1, SETWISEO:def 2;
then ADD "**" SFpr is_a_unity_wrt ADD by BINOP_1:def 8;
then ( ASFpr . pr = 0 & ASFpr . pq = 0 & ASFpr . rq = 0 ) by A60;
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) ; :: thesis: verum

end;

suppose A127: len SFpr <> 0 ; :: thesis: ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq)

then len SFpr >= 1 by NAT_1:14;
then consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A128: ( F . 1 = SFpr . 1 & ( for n being Element of NAT st 0 <> n & n < len SFpr holds
F . (n + 1) = ADD . (F . n),(SFpr . (n + 1)) ) & ADD "**" SFpr = F . (len SFpr) ) by FINSOP_1:def 1;
defpred S₉[ Element of NAT ] means ( $1 <> 0 & $1 <= len SFpr implies for F' being RealMap of [:T,T:] st F' = F . $1 holds
F' . pr <= (F' . pq) + (F' . rq) );
A129: S₉[ 0 ] ;
A130: for k being Element of NAT st S₉[k] holds
S₉[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume A131: S₉[k] ; :: thesis: S₉[k + 1]
assume A132: ( k + 1 <> 0 & k + 1 <= len SFpr ) ; :: thesis: for F' being RealMap of [:T,T:] st F' = F . (k + 1) holds
F' . pr <= (F' . pq) + (F' . rq)
then A133: ( k + 1 <= len SFpr & k < len SFpr & k + 1 >= 1 ) by NAT_1:13, NAT_1:14;
then A134: k + 1 in dom SFpr by FINSEQ_3:27;
consider x, y being Point of T such that
A135: ( [x,y] = pr & rng SFpr = H₄(H₃(x) \/ H₃(y)) ) by A43;
SFpr . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A134, A135, FUNCT_1:def 5;
then consider fd being RealMap of T such that
A136: ( Fdist . fd = SFpr . (k + 1) & fd in H₃(x) \/ H₃(y) ) ;
fd in Funcs the carrier of T,REAL by FUNCT_2:11;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SFpr . (k + 1) as RealMap of [:T,T:] by A136, FUNCT_2:7, FUNCT_2:121;
( (fd . p) - (fd . r) = ((fd . p) - (fd . q)) + ((fd . q) - (fd . r)) & fd in Funcs the carrier of T,REAL ) by FUNCT_2:11;
then A137: ( abs ((fd . p) - (fd . r)) <= (abs ((fd . p) - (fd . q))) + (abs ((fd . q) - (fd . r))) & abs ((fd . q) - (fd . r)) = abs (- ((fd . q) - (fd . r))) & Fdistfd . p,r = abs ((fd . p) - (fd . r)) & Fdistfd . p,q = abs ((fd . p) - (fd . q)) & Fdistfd . r,q = abs ((fd . r) - (fd . q)) ) by A29, COMPLEX1:138, COMPLEX1:142;
let F' be RealMap of [:T,T:]; :: thesis: ( F' = F . (k + 1) implies F' . pr <= (F' . pq) + (F' . rq) )
assume A138: F' = F . (k + 1) ; :: thesis: F' . pr <= (F' . pq) + (F' . rq)

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: F' . pr <= (F' . pq) + (F' . rq)

hence F' . pr <= (F' . pq) + (F' . rq) by A128, A136, A137, A138; :: thesis: verum

end;

suppose k > 0 ; :: thesis: F' . pr <= (F' . pq) + (F' . rq)

then ( Fk1 = ADD . Fk,SFk1 & k > 0 ) by A128, A133;
then ( Fk1 = Fk + SFk1 & Fk . pr <= (Fk . pq) + (Fk . rq) & Fdistfd = SFk1 ) by A46, A131, A132, A136, NAT_1:13;
then ( (Fk . pr) + (SFk1 . pr) <= ((Fk . pq) + (Fk . rq)) + ((SFk1 . pq) + (SFk1 . rq)) & Fk1 . pr = (Fk . pr) + (SFk1 . pr) & Fk1 . pq = (Fk . pq) + (SFk1 . pq) & Fk1 . rq = (Fk . rq) + (SFk1 . rq) ) by A137, NAGATA_1:def 7, XREAL_1:9;
hence F' . pr <= (F' . pq) + (F' . rq) by A138; :: thesis: verum

end;

end;

end;

for n being Element of NAT holds S₉[n] from NAT_1:sch 1(A129, A130);
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A127, A128; :: thesis: verum

end;

end;

end;

then ( ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) & SumFpr = ADD "**" SFpr & SumFpr . pq <= SumFpq . pq & SumFpr . rq <= SumFrq . rq ) by A48, A61;
then ( SumFpr . pr <= (SumFpr . pq) + (SumFpr . rq) & (SumFpr . pq) + (SumFpr . rq) <= (SumFpq . pq) + (SumFrq . rq) ) by XREAL_1:9;
then ( SumFpr . pr <= (SumFpq . pq) + (SumFrq . rq) & SumFTS . pr = SumFpr . pr & SumFTS . pq = SumFpq . pq ) by NAGATA_1:def 8, XXREAL_0:2;
hence SumFTS . p,r <= (SumFTS . p,q) + (SumFTS . r,q) by NAGATA_1:def 8; :: thesis: verum

end;

end;

then A139: SumFTS is_a_pseudometric_of the carrier of T by NAGATA_1:28;
A140: for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
SumFTS' . [p,q] >= 1

proof

let p, q be Point of T; :: thesis: ( ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies SumFTS' . [p,q] >= 1 )
assume A141: ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; :: thesis: SumFTS' . [p,q] >= 1
reconsider pq = [p,q] as Point of [:T,T:] by BORSUK_1:def 5;
reconsider SF = SFdist . pq as FinSequence of Funcs the carrier of [:T,T:],REAL by FINSEQ_1:def 11;
reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:121;
assume A142: SumFTS' . [p,q] < 1 ; :: thesis: contradiction
A143: ( SumFTS . pq = SumFTS . p,q & SumFTS . pq = (SumFdist . pq) . pq & SumFdist . pq = ASF ) by A48, NAGATA_1:def 8;
consider x, y being Point of T such that
A144: ( [x,y] = pq & rng SF = H₄(H₃(x) \/ H₃(y)) ) by A43;
consider A, B being Subset of T such that
A145: ( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) by A141;
reconsider FnB = Fn . B as RealMap of T by A145, FUNCT_2:7, FUNCT_2:121;
A in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= B ) } by A145;
then A c= H₁(B) by ZFMISC_1:92;
then ( A c= Vm . B & Vm . B c= Cl (Vm . B) & q in the carrier of T \ B ) by A12, A145, PRE_TOPC:48, XBOOLE_0:def 5;
then A146: ( p in Cl (Vm . B) & q in B ` & Cl (Vm . B) c= B ) by A13, A145, TARSKI:def 3;
then ( p in Sx . p & p in B ) by A22;
then Sx . p meets B by XBOOLE_0:3;
then ( B in H₂(Sx . p) & x = p ) by A144, A145, ZFMISC_1:33;
then FnB in H₃(x) by A145;
then FnB in H₃(x) \/ H₃(y) by XBOOLE_0:def 3;
then A147: Fdist . FnB in rng SF by A144;
then SF <> {} by RELAT_1:60;
then len SF <> 0 ;
then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A148: ( F . 1 = SF . 1 & ( for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . (F . n),(SF . (n + 1)) ) & ADD "**" SF = F . (len SF) ) by FINSOP_1:def 1;
A149: for k being Element of NAT st k <> 0 & k <= len SF holds
for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0

proof

let k be Element of NAT ; :: thesis: ( k <> 0 & k <= len SF implies for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0 )
assume A150: ( k <> 0 & k <= len SF ) ; :: thesis: for f being RealMap of [:T,T:] st f = SF . k holds
f . pq >= 0
let f be RealMap of [:T,T:]; :: thesis: ( f = SF . k implies f . pq >= 0 )
assume A151: f = SF . k ; :: thesis: f . pq >= 0
( k >= 1 & k <= len SF ) by A150, NAT_1:14;
then k in dom SF by FINSEQ_3:27;
then SF . k in H₄(H₃(x) \/ H₃(y)) by A144, FUNCT_1:def 5;
then consider fd being RealMap of T such that
A152: ( Fdist . fd = SF . k & fd in H₃(x) \/ H₃(y) ) ;
( Fdist . fd = f & fd in Funcs the carrier of T,REAL ) by A151, A152, FUNCT_2:11;
then f . p,q = abs ((fd . p) - (fd . q)) by A29;
hence f . pq >= 0 by COMPLEX1:132; :: thesis: verum

end;

defpred S₉[ Element of NAT ] means for k being Element of NAT st k <> 0 & k <= $1 & $1 <= len SF holds
for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . $1 holds
fk . pq <= Fn . pq;
A153: S₉[ 0 ] ;
A154: for i being Element of NAT st S₉[i] holds
S₉[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₉[i] implies S₉[i + 1] )
assume A155: S₉[i] ; :: thesis: S₉[i + 1]
let k be Element of NAT ; :: thesis: ( k <> 0 & k <= i + 1 & i + 1 <= len SF implies for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq )
assume A156: ( k <> 0 & k <= i + 1 & i + 1 <= len SF ) ; :: thesis: for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq

now

let fk, Fn be RealMap of [:T,T:]; :: thesis: ( fk = SF . k & Fn = F . (i + 1) implies b₁ . pq <= b₂ . pq )
assume A157: ( fk = SF . k & Fn = F . (i + 1) ) ; :: thesis: b₁ . pq <= b₂ . pq
reconsider Fi = F . i as RealMap of [:T,T:] by FUNCT_2:121;
1 <= i + 1 by NAT_1:14;
then i + 1 in dom SF by A156, FINSEQ_3:27;
then SF . (i + 1) in rng SF by FUNCT_1:def 5;
then reconsider SFi1 = SF . (i + 1) as RealMap of [:T,T:] by FUNCT_2:121;

per cases ( k < i + 1 or k = i + 1 ) by A156, XXREAL_0:1;

suppose k < i + 1 ; :: thesis: b₁ . pq <= b₂ . pq

then ( k <= i & i <= len SF & i < i + 1 ) by A156, NAT_1:13;
then A158: ( fk . pq <= Fi . pq & i <> 0 & i < len SF & i + 1 <> 0 ) by A155, A156, A157, XXREAL_0:2;
then ( F . (i + 1) = ADD . (F . i),(SF . (i + 1)) & SFi1 . pq >= 0 ) by A148, A149, A156;
then ( Fn = Fi + SFi1 & (Fi . pq) + 0 <= (Fi . pq) + (SFi1 . pq) ) by A46, A157, XREAL_1:9;
then Fn . pq >= Fi . pq by NAGATA_1:def 7;
hence fk . pq <= Fn . pq by A158, XXREAL_0:2; :: thesis: verum

end;

suppose A159: k = i + 1 ; :: thesis: b₁ . pq <= b₂ . pq

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: b₁ . pq <= b₂ . pq

hence fk . pq <= Fn . pq by A148, A157, A159; :: thesis: verum

end;

suppose A160: i <> 0 ; :: thesis: b₁ . pq <= b₂ . pq

i + 0 < i + 1 by XREAL_1:10;
then A161: ( i < len SF & 1 <= i ) by A156, A160, NAT_1:14, XXREAL_0:2;
then i in dom SF by FINSEQ_3:27;
then SF . i in rng SF by FUNCT_1:def 5;
then reconsider SFi = SF . i as RealMap of [:T,T:] by FUNCT_2:121;
( 0 <= SFi . pq & SFi . pq <= Fi . pq ) by A149, A155, A161;
then ( F . (i + 1) = ADD . (F . i),(SF . (i + 1)) & fk = SFi1 & 0 <= Fi . pq ) by A148, A157, A159, A161;
then ( Fn = Fi + fk & (Fi . pq) + (fk . pq) >= 0 + (fk . pq) ) by A46, A157, XREAL_1:9;
hence fk . pq <= Fn . pq by NAGATA_1:def 7; :: thesis: verum

end;

end;

end;

end;

end;

hence for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds
fk . pq <= Fn . pq ; :: thesis: verum

end;

A162: for i being Element of NAT holds S₉[i] from NAT_1:sch 1(A153, A154);
reconsider FdistFnB = Fdist . FnB as RealMap of [:T,T:] by A147, FUNCT_2:121;
S₂[B,Fn . B] by A20, A145;
then ( FnB in Funcs the carrier of T,REAL & FnB . p = 1 & FnB . q = 0 ) by A145, A146, FUNCT_2:7;
then A163: ( FdistFnB . p,q = abs (1 - 0 ) & abs 1 = 1 ) by A29, ABSVALUE:def 1;
consider k being set such that
A164: ( k in dom SF & SF . k = Fdist . FnB ) by A147, FUNCT_1:def 5;
A165: k in Seg (len SF) by A164, FINSEQ_1:def 3;
reconsider k = k as Element of NAT by A164;
( k <> 0 & k <= len SF & FdistFnB = SF . k & ASF = F . (len SF) ) by A148, A164, A165, FINSEQ_1:3;
hence contradiction by A142, A143, A162, A163; :: thesis: verum

end;

take pmet' = min 1,SumFTS'; :: thesis: S₁[n,m,pmet']
A166: ( min 1,SumFTS' = min 1,SumFTS & min 1,SumFTS' is continuous & min 1,SumFTS is_a_pseudometric_of the carrier of T ) by A113, A139, BORSUK_1:def 5, NAGATA_1:27, NAGATA_1:30;
A167: for p, q being Point of T holds (min 1,SumFTS') . [p,q] <= 1

proof

let p, q be Point of T; :: thesis: (min 1,SumFTS') . [p,q] <= 1
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
then (min 1,SumFTS') . [p,q] = min 1,(SumFTS' . [p,q]) by NAGATA_1:def 9;
hence (min 1,SumFTS') . [p,q] <= 1 by XXREAL_0:17; :: thesis: verum

end;

now

let p, q be Point of T; :: thesis: ( ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies 1 = (min 1,SumFTS') . [p,q] )
assume ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; :: thesis: 1 = (min 1,SumFTS') . [p,q]
then SumFTS' . [p,q] >= 1 by A140;
then ( 1 = min 1,(SumFTS' . [p,q]) & [:the carrier of T,the carrier of T:] = the carrier of [:T,T:] ) by BORSUK_1:def 5, XXREAL_0:def 9;
hence 1 = (min 1,SumFTS') . [p,q] by NAGATA_1:def 9; :: thesis: verum

end;

hence S₁[n,m,pmet'] by A166, A167; :: thesis: verum

end;

defpred S₂[ set , set ] means ex F being RealMap of [:T,T:] st
( F = $2 & ( for n, m being Element of NAT st (PairFunc " ) . $1 = [n,m] holds
S₁[n,m,F] ) );
A168: for k being set st k in NAT holds
ex f being set st
( f in Funcs the carrier of [:T,T:],REAL & S₂[k,f] )

proof

let k be set ; :: thesis: ( k in NAT implies ex f being set st
( f in Funcs the carrier of [:T,T:],REAL & S₂[k,f] ) )
assume A169: k in NAT ; :: thesis: ex f being set st
( f in Funcs the carrier of [:T,T:],REAL & S₂[k,f] )
A170: ( PairFunc is onto & PairFunc is one-to-one ) by Th2;
then NAT = rng PairFunc by FUNCT_2:def 3;
then consider nm being set such that
A171: ( nm in dom PairFunc & k = PairFunc . nm ) by A169, FUNCT_1:def 5;
consider n, m being set such that
A172: ( n in NAT & m in NAT & nm = [n,m] ) by A171, ZFMISC_1:def 2;
consider pmet' being RealMap of [:T,T:] such that
A173: S₁[n,m,pmet'] by A6, A172;
take pmet' ; :: thesis: ( pmet' in Funcs the carrier of [:T,T:],REAL & S₂[k,pmet'] )
thus pmet' in Funcs the carrier of [:T,T:],REAL by FUNCT_2:11; :: thesis: S₂[k,pmet']
take pm = pmet'; :: thesis: ( pm = pmet' & ( for n, m being Element of NAT st (PairFunc " ) . k = [n,m] holds
S₁[n,m,pm] ) )
thus pm = pmet' ; :: thesis: for n, m being Element of NAT st (PairFunc " ) . k = [n,m] holds
S₁[n,m,pm]
let n1, m1 be Element of NAT ; :: thesis: ( (PairFunc " ) . k = [n1,m1] implies S₁[n1,m1,pm] )
assume (PairFunc " ) . k = [n1,m1] ; :: thesis: S₁[n1,m1,pm]
then [n1,m1] = [n,m] by A170, A171, A172, Lm3, FUNCT_1:54;
then ( n1 = n & m1 = m ) by ZFMISC_1:33;
hence S₁[n1,m1,pm] by A173; :: thesis: verum

end;

consider F being Function of NAT ,(Funcs the carrier of [:T,T:],REAL ) such that
A174: for n being set st n in NAT holds
S₂[n,F . n] from FUNCT_2:sch 1(A168);
A175: dom F = NAT by FUNCT_2:def 1;

now

let n be Element of NAT ; :: thesis: F . n is PartFunc of [:the carrier of T,the carrier of T:],REAL
( F . n in Funcs the carrier of [:T,T:],REAL & [:the carrier of T,the carrier of T:] = the carrier of [:T,T:] ) by BORSUK_1:def 5;
hence F . n is PartFunc of [:the carrier of T,the carrier of T:],REAL by FUNCT_2:121; :: thesis: verum

end;

then reconsider F' = F as Functional_Sequence of [:the carrier of T,the carrier of T:],REAL by A175, SEQFUNC:1;
A176: for k being Element of NAT ex pmet being Function of [:the carrier of T,the carrier of T:],REAL st
( F' . k = 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 <= 1 ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) )

proof

let k be Element of NAT ; :: thesis: ex pmet being Function of [:the carrier of T,the carrier of T:],REAL st
( F' . k = 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 <= 1 ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) )
A177: ( PairFunc is onto & PairFunc is one-to-one ) by Th2;
then NAT = rng PairFunc by FUNCT_2:def 3;
then consider nm being set such that
A178: ( nm in dom PairFunc & k = PairFunc . nm ) by FUNCT_1:def 5;
consider n, m being set such that
A179: ( n in NAT & m in NAT & nm = [n,m] ) by A178, ZFMISC_1:def 2;
A180: [n,m] = (PairFunc " ) . k by A177, A178, A179, Lm3, FUNCT_1:54;
consider Fk being RealMap of [:T,T:] such that
A181: ( Fk = F . k & ( for n, m being Element of NAT st (PairFunc " ) . k = [n,m] holds
S₁[n,m,Fk] ) ) by A174;
consider pmet being Function of [:the carrier of T,the carrier of T:],REAL such that
A182: ( Fk = pmet & Fk is continuous & pmet is_a_pseudometric_of the carrier of T & ( for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) ) ) by A179, A180, A181;
take pmet ; :: thesis: ( F' . k = 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 <= 1 ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) )
thus ( F' . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A181, A182; :: thesis: ( ( for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq <= 1 ) & ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) )
thus for pq being Element of [:the carrier of T,the carrier of T:] holds pmet . pq <= 1 :: thesis: for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous

proof

let pq be Element of [:the carrier of T,the carrier of T:]; :: thesis: pmet . pq <= 1
consider p, q being set such that
A183: ( p in the carrier of T & q in the carrier of T & pq = [p,q] ) by ZFMISC_1:def 2;
thus pmet . pq <= 1 by A182, A183; :: thesis: verum

end;

thus for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous by A182; :: thesis: verum

end;

for p being Point of T
for A' being non empty Subset of T st not p in A' & A' is closed holds
ex k being Element of NAT st
for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . k = pmet holds
(inf pmet,A') . p > 0

proof

let p be Point of T; :: thesis: for A' being non empty Subset of T st not p in A' & A' is closed holds
ex k being Element of NAT st
for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . k = pmet holds
(inf pmet,A') . p > 0
let A' be non empty Subset of T; :: thesis: ( not p in A' & A' is closed implies ex k being Element of NAT st
for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . k = pmet holds
(inf pmet,A') . p > 0 )
assume A184: ( not p in A' & A' is closed ) ; :: thesis: ex k being Element of NAT st
for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . k = pmet holds
(inf pmet,A') . p > 0
set O = A' ` ;
( p in A' ` & A' ` is open ) by A184, XBOOLE_0:def 5;
then consider U being Subset of T such that
A185: ( p in U & Cl U c= A' ` & U in Union Bn ) by A1, A5, NAGATA_1:19;
Union Bn c= the topology of T by A5, CANTOR_1:def 2;
then reconsider U = U as open Subset of T by A185, PRE_TOPC:def 5;
consider W being Subset of T such that
A186: ( p in W & Cl W c= U & W in Union Bn ) by A1, A5, A185, NAGATA_1:19;
Union Bn c= the topology of T by A5, CANTOR_1:def 2;
then reconsider W = W as open Subset of T by A186, PRE_TOPC:def 5;
consider n being Element of NAT such that
A187: U in Bn . n by A185, PROB_1:25;
consider m being Element of NAT such that
A188: W in Bn . m by A186, PROB_1:25;
set k = PairFunc . [n,m];
take PairFunc . [n,m] ; :: thesis: for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . (PairFunc . [n,m]) = pmet holds
(inf pmet,A') . p > 0
reconsider Fk = F . (PairFunc . [n,m]) as RealMap of [:T,T:] by FUNCT_2:121;
dom PairFunc = [:NAT ,NAT :] by FUNCT_2:def 1;
then ( PairFunc is one-to-one & [n,m] in dom PairFunc ) by Th2;
then A189: [n,m] = (PairFunc " ) . (PairFunc . [n,m]) by Lm3, FUNCT_1:54;
consider G being RealMap of [:T,T:] such that
A190: ( G = F . (PairFunc . [n,m]) & ( for n, m being Element of NAT st (PairFunc " ) . (PairFunc . [n,m]) = [n,m] holds
S₁[n,m,G] ) ) by A174;
consider pmet being Function of [:the carrier of T,the carrier of T:],REAL such that
A191: ( G = pmet & G is continuous & pmet is_a_pseudometric_of the carrier of T & ( for p, q being Point of T holds
( pmet . [p,q] <= 1 & ( for p, q being Point of T st ex A, B being Subset of T st
( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) holds
pmet . [p,q] = 1 ) ) ) ) by A189, A190;
consider a being set such that
A192: a in A' by XBOOLE_0:def 1;
( a in A' & the carrier of T = dom (dist pmet,p) ) by A192, FUNCT_2:def 1;
then A193: (dist pmet,p) . a in (dist pmet,p) .: A' by FUNCT_1:def 12;
for rn being real number st rn in (dist pmet,p) .: A' holds
rn >= 1

proof

let rn be real number ; :: thesis: ( rn in (dist pmet,p) .: A' implies rn >= 1 )
assume rn in (dist pmet,p) .: A' ; :: thesis: rn >= 1
then consider a being set such that
A194: ( a in dom (dist pmet,p) & a in A' & rn = (dist pmet,p) . a ) by FUNCT_1:def 12;
reconsider a = a as Point of T by A194;
( U c= Cl U & Cl U c= A' ` ) by A185, PRE_TOPC:48;
then U c= A' ` by XBOOLE_1:1;
then U misses A' by SUBSET_1:43;
then not a in U by A194, XBOOLE_0:3;
then ( Fk . [p,a] = 1 & pmet . p,a = (dist pmet,p) . a ) by A186, A187, A188, A190, A191, Def2;
hence rn >= 1 by A190, A191, A194; :: thesis: verum

end;

then ( inf ((dist pmet,p) .: A') >= 1 & pmet is bounded_below ) by A191, A193, Lm1, SEQ_4:60;
hence for pmet being Function of [:the carrier of T,the carrier of T:],REAL st F' . (PairFunc . [n,m]) = pmet holds
(inf pmet,A') . p > 0 by A190, A191, Def3; :: thesis: verum

end;

hence T is metrizable by A2, A176, Th17; :: thesis: verum

end;

thus ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) ) by NAGATA_1:15, NAGATA_1:16; :: thesis: verum