let T be non empty TopSpace; :: thesis:
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:

set cTT = the carrier of [:T,T:];
set bcT = bool the carrier of T;
set cT = the carrier of T;
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:
set Fun = Funcs ( the carrier of [:T,T:],REAL);
consider Bn being FamilySequence of T such that
A4: Bn is Basis_sigma_locally_finite by A3;
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 ) ) ) );
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] ) );
A5: Union Bn is Basis of T by A4, NAGATA_1:def 6;
A6: Bn is sigma_locally_finite by A4, NAGATA_1:def 6;
A7: for n, m being Element of NAT ex pmet9 being RealMap of [:T,T:] st S₁[n,m,pmet9]

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;
defpred S₄[ RealMap of T, Function] means for p, q being Point of T holds $2 . (p,q) = abs (($1 . p) - ($1 . q));
let n, m be Element of NAT ; :: thesis:
deffunc H₁( set ) -> set = union { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= $1 ) } ;
set Bnn = Bn . n;
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 );
A8: for A being set st A in bool the carrier of T holds
H₁(A) in bool the carrier of T

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

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

end;

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

end;

consider Vm being Function of (bool the carrier of T),(bool the carrier of T) such that
A11: for A being set st A in bool the carrier of T holds
Vm . A = H₁(A) from FUNCT_2:sch 2(A8);
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 ) ) ) );
A12: Bn . m is locally_finite by A6, NAGATA_1:def 3;
A13: for A being Subset of T holds Cl (Vm . A) c= A

let A be Subset of T; :: thesis:
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

let B be set ; :: according to TARSKI:def 3 :: thesis:
assume B in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= A ) } ; :: thesis:
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:

end;

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

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

end;

VmA c= Bn . m

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

end;

then Cl (union VmA) = union (clf VmA) by A12, PCOMPS_1:9, PCOMPS_1:20;
hence Cl (Vm . A) c= A by A11, A14; :: thesis:

end;

A19: 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] )

let A be set ; :: thesis:
assume A in Bn . n ; :: thesis:
then A20: A in Union Bn by PROB_1:12;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider A = A as open Subset of T by A20, PRE_TOPC:def 2;
A ` misses A by XBOOLE_1:79;
then A21: A ` misses Cl (Vm . A) by A13, XBOOLE_1:63;
T is normal by A1, A4, NAGATA_1:20;
then consider f being Function of T,R^1 such that
A22: ( 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 A21, URYSOHN3:20;
reconsider f9 = f as RealMap of T by TOPMETR:17;
A23: ex F being RealMap of T ex S being Subset of T st
( S = A & F = f9 & 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 f9 ; :: thesis:
take A ; :: thesis:
thus ( A = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds
( 0 <= f9 . p & f9 . p <= 1 & ( p in A ` implies f9 . p = 0 ) & ( p in Cl (Vm . A) implies f9 . p = 1 ) ) ) ) by A22, TOPREAL6:74; :: thesis:

end;

f9 in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
hence ex f being set st
( f in Funcs ( the carrier of T,REAL) & S₆[A,f] ) by A23; :: thesis:

end;

consider Fn being Function of (Bn . n),(Funcs ( the carrier of T,REAL)) such that
A24: for A being set st A in Bn . n holds
S₆[A,Fn . A] from FUNCT_2:sch 1(A19);
Bn . n is locally_finite by A6, NAGATA_1:def 3;
then A25: for p being Element of the carrier of T ex A being Element of bool the carrier of T st S₅[p,A] by PCOMPS_1:def 1;
consider Sx being Function of the carrier of T,(bool the carrier of T) such that
A26: for p being Element of the carrier of T holds S₅[p,Sx . p] from FUNCT_2:sch 3(A25);
defpred S₇[ set , set ] means for x, y being Element of T st $1 = [x,y] holds
$2 = [:(Sx . x),(Sx . y):];
A27: for pq9 being set st pq9 in the carrier of [:T,T:] holds
ex SS being set st
( SS in bool the carrier of [:T,T:] & S₇[pq9,SS] )

let pq9 be set ; :: thesis:
assume pq9 in the carrier of [:T,T:] ; :: thesis:
then pq9 in [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then consider p, q being set such that
A28: ( p in the carrier of T & q in the carrier of T ) and
A29: pq9 = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A28;

let p1, q1 be Point of T; :: thesis:
assume A30: pq9 = [p1,q1] ; :: thesis:
then p1 = p by A29, ZFMISC_1:27;
hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] by A29, A30, ZFMISC_1:27; :: thesis:

end;

hence ex SS being set st
( SS in bool the carrier of [:T,T:] & S₇[pq9,SS] ) ; :: thesis:

end;

consider SS being Function of the carrier of [:T,T:],(bool the carrier of [:T,T:]) such that
A31: for pq being set st pq in the carrier of [:T,T:] holds
S₇[pq,SS . pq] from FUNCT_2:sch 1(A27);
A32: for pq9 being Point of [:T,T:] holds
( pq9 in SS . pq9 & SS . pq9 is open )

let pq9 be Point of [:T,T:]; :: thesis:
pq9 in the carrier of [:T,T:] ;
then pq9 in [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then consider p, q being set such that
A33: ( p in the carrier of T & q in the carrier of T ) and
A34: pq9 = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A33;
A35: ( p in Sx . p & q in Sx . q ) by A26;
A36: ( Sx . p is open & Sx . q is open ) by A26;
SS . pq9 = [:(Sx . p),(Sx . q):] by A31, A34;
hence ( pq9 in SS . pq9 & SS . pq9 is open ) by A34, A35, A36, BORSUK_1:6, ZFMISC_1:def 2; :: thesis:

end;

A37: 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]

let f, g be Element of Funcs ( the carrier of [:T,T:],REAL); :: thesis:
set f9 = f;
set g9 = g;
f + g in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
hence ex fg being Element of Funcs ( the carrier of [:T,T:],REAL) st S₃[f,g,fg] ; :: thesis:

end;

consider ADD being BinOp of (Funcs ( the carrier of [:T,T:],REAL)) such that
A38: 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(A37);
A39: 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]

let f be Element of Funcs ( the carrier of T,REAL); :: thesis:
defpred S₈[ Element of T, Element of T, set ] means $3 = abs ((f . $1) - (f . $2));
A40: 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
A41: for x, y being Element of the carrier of T holds S₈[x,y,Fd . (x,y)] from BINOP_1:sch 3(A40);
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;
then Fd in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
hence ex fxy being Element of Funcs ( the carrier of [:T,T:],REAL) st S₄[f,fxy] by A41; :: thesis:

end;

consider Fdist being Function of (Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)) such that
A42: for fd being Element of Funcs ( the carrier of T,REAL) holds S₄[fd,Fdist . fd] from FUNCT_2:sch 3(A39);
deffunc H₃( Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & A in H₂(Sx . $1) ) } ;
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)) ) );
A43: for p being Point of T holds H₃(p) is finite

deffunc H₅( Subset of T) -> set = Fn . $1;
let p be Point of T; :: thesis:
set SFxx = { H₅(A) where A is Subset of T : A in H₂(Sx . p) } ;
A44: H₃(p) c= { H₅(A) where A is Subset of T : A in H₂(Sx . p) }

let FA be set ; :: according to TARSKI:def 3 :: thesis:
assume FA in H₃(p) ; :: thesis:
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:

end;

A45: H₂(Sx . p) is finite by A26;
{ H₅(A) where A is Subset of T : A in H₂(Sx . p) } is finite from FRAENKEL:sch 21(A45);
hence H₃(p) is finite by A44; :: thesis:

end;

A46: 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) )

deffunc H₅( RealMap of T) -> set = Fdist . $1;
let p, q be Point of T; :: thesis:
A47: H₄(H₃(p) \/ H₃(q)) c= Funcs ( the carrier of [:T,T:],REAL)

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

end;

set RNG9 = { H₅(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H₃(p) \/ H₃(q) } ;
A49: 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) }

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

end;

( H₃(p) is finite & H₃(q) is finite ) by A43;
then A51: H₃(p) \/ H₃(q) is finite ;
{ 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(A51);
hence ( H₄(H₃(p) \/ H₃(q)) is finite & H₄(H₃(p) \/ H₃(q)) c= Funcs ( the carrier of [:T,T:],REAL) ) by A47, A49; :: thesis:

end;

A52: 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]

let pq be Element of the carrier of [:T,T:]; :: thesis:
pq in the carrier of [:T,T:] ;
then pq in [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then consider p, q being set such that
A53: ( p in the carrier of T & q in the carrier of T ) and
A54: pq = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A53;
consider SF being FinSequence such that
A55: rng SF = H₄(H₃(p) \/ H₃(q)) and
A56: SF is one-to-one by A46, FINSEQ_4:58;
rng SF c= Funcs ( the carrier of [:T,T:],REAL) by A46, A55;
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)) * by FINSEQ_1:def 11;
hence ex G being Element of (Funcs ( the carrier of [:T,T:],REAL)) * st S₈[pq,G] by A54, A55, A56; :: thesis:

end;

consider SFdist being Function of the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *) such that
A57: for pq being Element of the carrier of [:T,T:] holds S₈[pq,SFdist . pq] from FUNCT_2:sch 3(A52);
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;
A58: 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] )

let pq be set ; :: thesis:
assume pq in the carrier of [:T,T:] ; :: thesis:
then SFdist . pq in (Funcs ( the carrier of [:T,T:],REAL)) * by FUNCT_2:5;
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:

end;

consider SumFdist being Function of the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)) such that
A59: for xy being set st xy in the carrier of [:T,T:] holds
S₉[xy,SumFdist . xy] from FUNCT_2:sch 1(A58);
reconsider SumFdist9 = SumFdist as Function of the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:], the carrier of R^1)) by TOPMETR:17;
reconsider SumFTS9 = SumFdist9 Toler as RealMap of [:T,T:] by TOPMETR:17;
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then reconsider SumFTS = SumFdist9 Toler as Function of [: the carrier of T, the carrier of T:],REAL by TOPMETR:17;
A60: for f1, f2 being RealMap of [:T,T:] holds ADD . (f1,f2) = f1 + f2

let f1, f2 be RealMap of [:T,T:]; :: thesis:
reconsider f19 = f1, f29 = f2 as Element of Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8;
ADD . (f19,f29) = f19 + f29 by A38;
hence ADD . (f1,f2) = f1 + f2 ; :: thesis:

end;

A61: 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
SumFTS9 . [p,q] >= 1

let p, q be Point of T; :: thesis:
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:
then consider A, B being Subset of T such that
A is open and
B is open and
A62: A in Bn . m and
A63: B in Bn . n and
A64: p in A and
A65: Cl A c= B and
A66: not q in B ;
A67: S₆[B,Fn . B] by A24, A63;
A in { Q where Q is Subset of T : ( Q in Bn . m & Cl Q c= B ) } by A62, A65;
then A c= H₁(B) by ZFMISC_1:74;
then A68: A c= Vm . B by A11;
Vm . B c= Cl (Vm . B) by PRE_TOPC:18;
then A69: p in Cl (Vm . B) by A64, A68, TARSKI:def 3;
( Cl (Vm . B) c= B & p in Sx . p ) by A13, A26;
then Sx . p meets B by A69, XBOOLE_0:3;
then A70: B in H₂(Sx . p) by A63;
reconsider pq = [p,q] as Point of [:T,T:] by BORSUK_1:def 2;
reconsider SF = SFdist . pq as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def 11;
consider x, y being Point of T such that
A71: [x,y] = pq and
A72: rng SF = H₄(H₃(x) \/ H₃(y)) by A57;
reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:66;
assume A73: SumFTS9 . [p,q] < 1 ; :: thesis:
reconsider FnB = Fn . B as RealMap of T by A63, FUNCT_2:5, FUNCT_2:66;
A74: FnB in Funcs ( the carrier of T,REAL) by A63, FUNCT_2:5;
q in B ` by A66, XBOOLE_0:def 5;
then A75: FnB . q = 0 by A67;
x = p by A71, ZFMISC_1:27;
then FnB in H₃(x) by A63, A70;
then FnB in H₃(x) \/ H₃(y) by XBOOLE_0:def 3;
then A76: Fdist . FnB in rng SF by A72;
then reconsider FdistFnB = Fdist . FnB as RealMap of [:T,T:] by FUNCT_2:66;
SF <> {} by A76, RELAT_1:38;
then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A77: F . 1 = SF . 1 and
A78: for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A79: ADD "**" SF = F . (len SF) by FINSOP_1:def 1;
A80: ( SumFTS . pq = (SumFdist . pq) . pq & SumFdist . pq = ASF ) by A59, NAGATA_1:def 8;
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;
A81: 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

let k be Element of NAT ; :: thesis:
assume that
A82: k <> 0 and
A83: k <= len SF ; :: thesis:
k >= 1 by A82, NAT_1:14;
then k in dom SF by A83, FINSEQ_3:25;
then SF . k in H₄(H₃(x) \/ H₃(y)) by A72, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A84: Fdist . fd = SF . k and
fd in H₃(x) \/ H₃(y) ;
let f be RealMap of [:T,T:]; :: thesis:
assume A85: f = SF . k ; :: thesis:
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then f . (p,q) = abs ((fd . p) - (fd . q)) by A42, A85, A84;
hence f . pq >= 0 by COMPLEX1:46; :: thesis:

end;

A86: for i being Element of NAT st S₁₀[i] holds
S₁₀[i + 1]

let i be Element of NAT ; :: thesis:
assume A87: S₁₀[i] ; :: thesis:
let k be Element of NAT ; :: thesis:
assume that
A88: k <> 0 and
A89: k <= i + 1 and
A90: i + 1 <= len SF ; :: thesis:

1 <= i + 1 by NAT_1:14;
then i + 1 in dom SF by A90, FINSEQ_3:25;
then SF . (i + 1) in rng SF by FUNCT_1:def 3;
then reconsider SFi1 = SF . (i + 1) as RealMap of [:T,T:] by FUNCT_2:66;
reconsider Fi = F . i as RealMap of [:T,T:] by FUNCT_2:66;
let fk, Fn be RealMap of [:T,T:]; :: thesis:
assume that
A91: fk = SF . k and
A92: Fn = F . (i + 1) ; :: thesis:

per cases by A89, XXREAL_0:1;

suppose A93: k < i + 1 ; :: thesis:

A94: i < len SF by A90, NAT_1:13;
i <> 0 by A88, A93, NAT_1:13;
then F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A78, A94;
then A95: Fn = Fi + SFi1 by A60, A92;
SFi1 . pq >= 0 by A81, A90;
then (Fi . pq) + 0 <= (Fi . pq) + (SFi1 . pq) by XREAL_1:7;
then A96: Fn . pq >= Fi . pq by A95, NAGATA_1:def 7;
A97: i <= len SF by A90, NAT_1:13;
k <= i by A93, NAT_1:13;
then fk . pq <= Fi . pq by A87, A88, A91, A97;
hence fk . pq <= Fn . pq by A96, XXREAL_0:2; :: thesis:

end;

suppose A98: k = i + 1 ; :: thesis:

suppose i = 0 ; :: thesis:

hence fk . pq <= Fn . pq by A77, A91, A92, A98; :: thesis:

end;

suppose A99: i <> 0 ; :: thesis:

i + 0 < i + 1 by XREAL_1:8;
then A100: i < len SF by A90, XXREAL_0:2;
1 <= i by A99, NAT_1:14;
then i in dom SF by A100, FINSEQ_3:25;
then SF . i in rng SF by FUNCT_1:def 3;
then reconsider SFi = SF . i as RealMap of [:T,T:] by FUNCT_2:66;
0 <= SFi . pq by A81, A99, A100;
then 0 <= Fi . pq by A87, A99, A100;
then A101: (Fi . pq) + (fk . pq) >= 0 + (fk . pq) by XREAL_1:7;
F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A78, A99, A100;
then Fn = Fi + fk by A60, A91, A92, A98;
hence fk . pq <= Fn . pq by A101, NAGATA_1:def 7; :: thesis:

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:

end;

A102: S₁₀[ 0 ] ;
A103: for i being Element of NAT holds S₁₀[i] from NAT_1:sch 1(A102, A86);
consider k being set such that
A104: k in dom SF and
A105: SF . k = Fdist . FnB by A76, FUNCT_1:def 3;
A106: k in Seg (len SF) by A104, FINSEQ_1:def 3;
FnB . p = 1 by A69, A67;
then A107: FdistFnB . (p,q) = abs (1 - 0) by A42, A74, A75;
reconsider k = k as Element of NAT by A104;
A108: abs 1 = 1 by ABSVALUE:def 1;
( k <> 0 & k <= len SF ) by A106, FINSEQ_1:1;
hence contradiction by A73, A80, A79, A103, A107, A108, A105; :: thesis:

end;

A109: now

let p, q be Point of T; :: thesis:
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:
then SumFTS9 . [p,q] >= 1 by A61;
then A110: 1 = min (1,(SumFTS9 . [p,q])) by XXREAL_0:def 9;
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;
hence 1 = (min (1,SumFTS9)) . [p,q] by A110, NAGATA_1:def 9; :: thesis:

end;

A111: for pq being Element of the carrier of [:T,T:]
for map9 being Element of Funcs ( the carrier of [:T,T:],REAL) st map9 is_a_unity_wrt ADD holds
map9 . pq = 0

let pq be Element of the carrier of [:T,T:]; :: thesis:
let map9 be Element of Funcs ( the carrier of [:T,T:],REAL); :: thesis:
assume map9 is_a_unity_wrt ADD ; :: thesis:
then ADD . (map9,map9) = map9 by BINOP_1:3;
then (map9 + map9) . pq = map9 . pq by A38;
then (map9 . pq) + (map9 . pq) = map9 . pq by NAGATA_1:def 7;
hence map9 . pq = 0 ; :: thesis:

end;

A112: 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 ) )

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 ) ) ) } ;
let pq1, pq2 be Point of [:T,T:]; :: thesis:
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
A113: [p1,q1] = pq1 and
A114: rng S1 = H₄(H₃(p1) \/ H₃(q1)) by A57;
A115: 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)

let p, q, p1, q1 be Point of T; :: thesis:
assume A116: [p,q] in SS . [p1,q1] ; :: thesis:
reconsider pq1 = [p1,q1] as Element of the carrier of [:T,T:] by BORSUK_1:def 2;
[:(Sx . p1),(Sx . q1):] = SS . pq1 by A31;
then A117: ( p in Sx . p1 & q in Sx . q1 ) by A116, ZFMISC_1:87;
let no0 be set ; :: according to TARSKI:def 3 :: thesis:
assume no0 in H₅(p,q) ; :: thesis:
then consider A being Subset of T such that
A118: no0 = Fn . A and
A119: A in Bn . n and
A120: for FnA being RealMap of T holds
( not Fn . A = FnA or FnA . p > 0 or FnA . q > 0 ) ;
reconsider FnA = Fn . A as RealMap of T by A119, FUNCT_2:5, FUNCT_2:66;
A121: ( FnA . p > 0 or FnA . q > 0 ) by A120;
S₆[A,Fn . A] by A24, A119;
then ( not p in the carrier of T \ A or not q in the carrier of T \ A ) by A121;
then ( p in A or q in A ) by XBOOLE_0:def 5;
then ( A meets Sx . p1 or A meets Sx . q1 ) by A117, XBOOLE_0:3;
then ( A in H₂(Sx . p1) or A in H₂(Sx . q1) ) by A119;
then ( FnA in H₃(p1) or FnA in H₃(q1) ) by A119;
hence no0 in H₃(p1) \/ H₃(q1) by A118, XBOOLE_0:def 3; :: thesis:

end;

A122: H₄(H₅(p1,q1)) c= H₄(H₃(p1) \/ H₃(q1))

( p1 in Sx . p1 & q1 in Sx . q1 ) by A26;
then [p1,q1] in [:(Sx . p1),(Sx . q1):] by ZFMISC_1:87;
then [p1,q1] in SS . [p1,q1] by A31;
then A123: H₅(p1,q1) c= H₃(p1) \/ H₃(q1) by A115;
let FD be set ; :: according to TARSKI:def 3 :: thesis:
assume FD in H₄(H₅(p1,q1)) ; :: thesis:
then ex fd being RealMap of T st
( FD = Fdist . fd & fd in H₅(p1,q1) ) ;
hence FD in H₄(H₃(p1) \/ H₃(q1)) by A123; :: thesis:

end;

A124: 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

let f be FinSequence of Funcs ( the carrier of [:T,T:],REAL); :: thesis:
let p, q, p1, q1 be Point of T; :: thesis:
assume A125: rng f = H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) ; :: thesis:
reconsider pq = [p,q] as Element of the carrier of [:T,T:] by BORSUK_1:def 2;

suppose A126: len f = 0 ; :: thesis:

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

end;

suppose A129: len f <> 0 ; :: thesis:

then len f >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A130: F . 1 = f . 1 and
A131: for n being Element of NAT st 0 <> n & n < len f holds
F . (n + 1) = ADD . ((F . n),(f . (n + 1))) and
A132: 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 );
A133: for k being Element of NAT st S₁₀[k] holds
S₁₀[k + 1]

let k be Element of NAT ; :: thesis:
assume A134: S₁₀[k] ; :: thesis:
assume that
k + 1 <> 0 and
A135: k + 1 <= len f ; :: thesis:
A136: k < len f by A135, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom f by A135, FINSEQ_3:25;
then A137: f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) by A125, FUNCT_1:def 3;
then f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) ;
then consider fd being RealMap of T such that
A138: Fdist . fd = f . (k + 1) and
A139: fd in H₃(p1) \/ H₃(q1) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, fk1 = f . (k + 1) as RealMap of [:T,T:] by A138, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A140: Fdistfd . (p,q) = abs ((fd . p) - (fd . q)) by A42;
A141: not f . (k + 1) in H₄(H₅(p,q)) by A137, XBOOLE_0:def 5;
A142: ( fd . p = 0 & fd . q = 0 )

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

per cases by A139, XBOOLE_0:def 3;

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

then consider A being Subset of T such that
A144: fd = Fn . A and
A145: A in Bn . n and
A in H₂(Sx . p1) ;
A146: S₆[A,Fn . A] by A24, A145;
not fd in H₅(p,q) by A141, A138;
then ex FnA being RealMap of T st
( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A144, A145;
hence contradiction by A143, A144, A146; :: thesis:

end;

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

then consider A being Subset of T such that
A147: fd = Fn . A and
A148: A in Bn . n and
A in H₂(Sx . q1) ;
A149: S₆[A,Fn . A] by A24, A148;
not fd in H₅(p,q) by A141, A138;
then ex FnA being RealMap of T st
( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A147, A148;
hence contradiction by A143, A147, A149; :: thesis:

end;

end;

end;

suppose k = 0 ; :: thesis:

hence (F . (k + 1)) . pq = 0 by A130, A138, A142, A140, ABSVALUE:2; :: thesis:

end;

suppose A150: k > 0 ; :: thesis:

then Fk1 = ADD . (Fk,fk1) by A131, A136;
then Fk1 = Fk + fk1 by A60;
then Fk1 . pq = 0 + (fk1 . pq) by A134, A135, A150, NAGATA_1:def 7, NAT_1:13;
hence (F . (k + 1)) . pq = 0 by A138, A142, A140, ABSVALUE:2; :: thesis:

end;

end;

end;

A151: S₁₀[ 0 ] ;
for n being Element of NAT holds S₁₀[n] from NAT_1:sch 1(A151, A133);
hence (ADD "**" f) . pq = 0 by A129, A132; :: thesis:

end;

end;

end;

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

end;

A152: H₄(H₃(p1) \/ H₃(q1)) is finite by A46;
then consider No being FinSequence such that
A153: rng No = H₄(H₅(p1,q1)) and
A154: No is one-to-one by A122, FINSEQ_4:58;
H₄(H₃(p1) \/ H₃(q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A46;
then A155: H₄(H₅(p1,q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A122, XBOOLE_1:1;
then reconsider No = No as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A153, FINSEQ_1:def 4;
consider p2, q2 being Point of T such that
A156: [p2,q2] = pq2 and
A157: rng S2 = H₄(H₃(p2) \/ H₃(q2)) by A57;
reconsider S1 = SFdist . pq1, S2 = SFdist . pq2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by FINSEQ_1:def 11;
set RNiS2 = H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2));
A158: S2 is one-to-one by A57;
A159: ( ADD is having_a_unity & ADD is commutative & ADD is associative ) by A60, NAGATA_1:23;
S1 is one-to-one by A57;
then consider S1No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S1No is one-to-one and
A160: rng S1No = (rng S1) \ (rng No) and
A161: ADD "**" S1 = ADD . ((ADD "**" No),(ADD "**" S1No)) by A114, A122, A153, A154, A159, Th18;
consider NoiS2 being FinSequence such that
A162: rng NoiS2 = H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) and
A163: NoiS2 is one-to-one by A122, A152, FINSEQ_4:58;
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 A155, XBOOLE_1:1;
then reconsider NoiS2 = NoiS2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A162, FINSEQ_1:def 4;
rng NoiS2 c= rng No by A153, A162, XBOOLE_1:17;
then consider NoNoiS2 being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
NoNoiS2 is one-to-one and
A164: rng NoNoiS2 = (rng No) \ (rng NoiS2) and
A165: ADD "**" No = ADD . ((ADD "**" NoiS2),(ADD "**" NoNoiS2)) by A154, A159, A163, Th18;
rng NoiS2 c= rng S2 by A157, A162, XBOOLE_1:17;
then consider S2No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S2No is one-to-one and
A166: rng S2No = (rng S2) \ (rng NoiS2) and
A167: ADD "**" S2 = ADD . ((ADD "**" NoiS2),(ADD "**" S2No)) by A159, A163, A158, 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:66;
rng S2No = H₄(H₃(p2) \/ H₃(q2)) \ H₄(H₅(p1,q1)) by A157, A162, A166, XBOOLE_1:47;
then A168: AS2No . pq1 = 0 by A124, A113;
ANo = ANoiS2 + ANoNoiS2 by A60, A165;
then A169: ANo . pq1 = (ANoiS2 . pq1) + (ANoNoiS2 . pq1) by NAGATA_1:def 7;
AS1 = ANo + AS1No by A60, A161;
then A170: AS1 . pq1 = (ANo . pq1) + (AS1No . pq1) by NAGATA_1:def 7;
AS2 = ANoiS2 + AS2No by A60, A167;
then A171: AS2 . pq1 = (ANoiS2 . pq1) + (AS2No . pq1) by NAGATA_1:def 7;
A172: AS1No . pq1 = 0 by A124, A113, A114, A153, A160;
thus ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) :: thesis:

A173: ADD is having_a_unity by A60, NAGATA_1:23;
then A174: ex f being Element of Funcs ( the carrier of [:T,T:],REAL) st f is_a_unity_wrt ADD by SETWISEO:def 2;
assume A175: pq1 in SS . pq2 ; :: thesis:

let FD be set ; :: thesis:
assume FD in H₄(H₅(p1,q1)) ; :: thesis:
then A176: ex fd being RealMap of T st
( FD = Fdist . fd & fd in H₅(p1,q1) ) ;
H₅(p1,q1) c= H₃(p2) \/ H₃(q2) by A115, A113, A156, A175;
hence FD in H₄(H₃(p2) \/ H₃(q2)) by A176; :: thesis:

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)) by XBOOLE_1:28;
then rng NoNoiS2 = {} by A153, A162, A164, XBOOLE_1:37;
then NoNoiS2 = {} by RELAT_1:41;
then len NoNoiS2 = 0 ;
then ADD "**" NoNoiS2 = the_unity_wrt ADD by A173, FINSOP_1:def 1;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by A174, BINOP_1:def 8;
then A177: AS1 . pq1 = AS2 . pq1 by A111, A170, A169, A171, A172, A168;
SumFdist . pq1 = AS1 by A59;
hence (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 by A59, A177; :: thesis:

end;

A178: ANoNoiS2 . (p1,q1) >= 0

set N = NoNoiS2;

suppose A179: len NoNoiS2 = 0 ; :: thesis:

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

end;

suppose A182: len NoNoiS2 <> 0 ; :: thesis:

then len NoNoiS2 >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A183: F . 1 = NoNoiS2 . 1 and
A184: for n being Element of NAT st 0 <> n & n < len NoNoiS2 holds
F . (n + 1) = ADD . ((F . n),(NoNoiS2 . (n + 1))) and
A185: 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 );
A186: for k being Element of NAT st S₁₀[k] holds
S₁₀[k + 1]

let k be Element of NAT ; :: thesis:
assume A187: S₁₀[k] ; :: thesis:
assume that
k + 1 <> 0 and
A188: k + 1 <= len NoNoiS2 ; :: thesis:
A189: k < len NoNoiS2 by A188, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom NoNoiS2 by A188, FINSEQ_3:25;
then NoNoiS2 . (k + 1) in (rng No) \ (rng NoiS2) by A164, FUNCT_1:def 3;
then NoNoiS2 . (k + 1) in H₄(H₅(p1,q1)) by A153, XBOOLE_0:def 5;
then consider fd being RealMap of T such that
A190: Fdist . fd = NoNoiS2 . (k + 1) and
fd in H₅(p1,q1) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, Nk1 = NoNoiS2 . (k + 1) as RealMap of [:T,T:] by A190, FUNCT_2:5, FUNCT_2:66;
A191: abs ((fd . p1) - (fd . q1)) >= 0 by COMPLEX1:46;
A192: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A193: Fdistfd . (p1,q1) = abs ((fd . p1) - (fd . q1)) by A42;

A194: now

suppose k = 0 ; :: thesis:

hence Fk1 . (p1,q1) >= 0 by A42, A183, A190, A192, A191; :: thesis:

end;

suppose A195: k > 0 ; :: thesis:

then Fk1 = ADD . (Fk,Nk1) by A184, A189;
then A196: Fk1 = Fk + Nk1 by A60;
Fk . (p1,q1) >= 0 by A187, A188, A195, NAT_1:13;
then 0 + 0 <= (Fk . (p1,q1)) + (Nk1 . (p1,q1)) by A190, A191, A193;
hence Fk1 . (p1,q1) >= 0 by A113, A196, NAGATA_1:def 7; :: thesis:

end;

end;

end;

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

end;

A197: S₁₀[ 0 ] ;
for n being Element of NAT holds S₁₀[n] from NAT_1:sch 1(A197, A186);
hence ANoNoiS2 . (p1,q1) >= 0 by A182, A185; :: thesis:

end;

end;

end;

A198: AS2 . (p1,q1) <= AS1 . (p1,q1) by A113, A178, A170, A169, A171, A172, A168, XREAL_1:7;
let SumFdist1, SumFdist2 be RealMap of [:T,T:]; :: thesis:
assume that
A199: SumFdist1 = SumFdist . pq1 and
A200: SumFdist2 = SumFdist . pq2 ; :: thesis:
SumFdist2 = AS2 by A59, A200;
hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A59, A113, A199, A198; :: thesis:

end;

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

end;

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

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

A201: now

suppose A202: len SF = 0 ; :: thesis:

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

end;

suppose A205: len SF <> 0 ; :: thesis:

then len SF >= 1 by NAT_1:14;
then consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A206: F . 1 = SF . 1 and
A207: for n being Element of NAT st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A208: 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 );
A209: for k being Element of NAT st S₁₀[k] holds
S₁₀[k + 1]

let k be Element of NAT ; :: thesis:
assume A210: S₁₀[k] ; :: thesis:
consider x, y being Point of T such that
[x,y] = pp and
A211: rng SF = H₄(H₃(x) \/ H₃(y)) by A57;
assume that
k + 1 <> 0 and
A212: k + 1 <= len SF ; :: thesis:
A213: k < len SF by A212, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SF by A212, FINSEQ_3:25;
then SF . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A211, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A214: Fdist . fd = SF . (k + 1) and
fd in H₃(x) \/ H₃(y) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SF . (k + 1) as RealMap of [:T,T:] by A214, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A215: Fdistfd . (p,p) = abs ((fd . p) - (fd . p)) by A42;

suppose k = 0 ; :: thesis:

hence (F . (k + 1)) . pp = 0 by A206, A214, A215, ABSVALUE:2; :: thesis:

end;

suppose A216: k > 0 ; :: thesis:

then Fk1 = ADD . (Fk,SFk1) by A207, A213;
then Fk1 = Fk + SFk1 by A60;
then Fk1 . pp = 0 + (SFk1 . pp) by A210, A212, A216, NAGATA_1:def 7, NAT_1:13;
hence (F . (k + 1)) . pp = 0 by A214, A215, ABSVALUE:2; :: thesis:

end;

end;

end;

A217: S₁₀[ 0 ] ;
for n being Element of NAT holds S₁₀[n] from NAT_1:sch 1(A217, A209);
hence (ADD "**" SF) . pp = 0 by A205, A208; :: thesis:

end;

end;

end;

SumFdist . pp = ADD "**" SF by A59;
hence SumFTS . (p,p) = 0 by A201, NAGATA_1:def 8; :: thesis:

end;

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

reconsider pr = [p,r], pq = [p,q], rq = [r,q] as Point of [:T,T:] by BORSUK_1:def 2;
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:66;
reconsider SumFpr = SumFdist . pr, SumFpq = SumFdist . pq, SumFrq = SumFdist . rq as RealMap of [:T,T:] by FUNCT_2:66;
A218: ( SumFTS . pr = SumFpr . pr & SumFTS . pq = SumFpq . pq ) by NAGATA_1:def 8;
( SumFpr . pq <= SumFpq . pq & SumFpr . rq <= SumFrq . rq ) by A112;
then A219: (SumFpr . pq) + (SumFpr . rq) <= (SumFpq . pq) + (SumFrq . rq) by XREAL_1:7;

A220: now

suppose A221: len SFpr = 0 ; :: thesis:

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

end;

suppose A225: len SFpr <> 0 ; :: thesis:

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

let k be Element of NAT ; :: thesis:
assume A230: S₁₀[k] ; :: thesis:
consider x, y being Point of T such that
[x,y] = pr and
A231: rng SFpr = H₄(H₃(x) \/ H₃(y)) by A57;
assume that
k + 1 <> 0 and
A232: k + 1 <= len SFpr ; :: thesis:
A233: k < len SFpr by A232, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SFpr by A232, FINSEQ_3:25;
then SFpr . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A231, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A234: Fdist . fd = SFpr . (k + 1) and
fd in H₃(x) \/ H₃(y) ;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then reconsider Fdistfd = Fdist . fd, Fk1 = F . (k + 1), Fk = F . k, SFk1 = SFpr . (k + 1) as RealMap of [:T,T:] by A234, FUNCT_2:5, FUNCT_2:66;
A235: (fd . p) - (fd . r) = ((fd . p) - (fd . q)) + ((fd . q) - (fd . r)) ;
then A236: abs ((fd . p) - (fd . r)) <= (abs ((fd . p) - (fd . q))) + (abs ((fd . q) - (fd . r))) by COMPLEX1:56;
A237: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A238: ( Fdistfd . (p,r) = abs ((fd . p) - (fd . r)) & Fdistfd . (p,q) = abs ((fd . p) - (fd . q)) ) by A42;
A239: ( abs ((fd . q) - (fd . r)) = abs (- ((fd . q) - (fd . r))) & Fdistfd . (r,q) = abs ((fd . r) - (fd . q)) ) by A42, A237, COMPLEX1:52;
let F9 be RealMap of [:T,T:]; :: thesis:
assume A240: F9 = F . (k + 1) ; :: thesis:

suppose k = 0 ; :: thesis:

hence F9 . pr <= (F9 . pq) + (F9 . rq) by A226, A234, A235, A238, A239, A240, COMPLEX1:56; :: thesis:

end;

suppose A241: k > 0 ; :: thesis:

then Fk . pr <= (Fk . pq) + (Fk . rq) by A230, A232, NAT_1:13;
then A242: (Fk . pr) + (SFk1 . pr) <= ((Fk . pq) + (Fk . rq)) + ((SFk1 . pq) + (SFk1 . rq)) by A234, A236, A238, A239, XREAL_1:7;
Fk1 = ADD . (Fk,SFk1) by A227, A233, A241;
then A243: Fk1 = Fk + SFk1 by A60;
then ( Fk1 . pq = (Fk . pq) + (SFk1 . pq) & Fk1 . rq = (Fk . rq) + (SFk1 . rq) ) by NAGATA_1:def 7;
hence F9 . pr <= (F9 . pq) + (F9 . rq) by A240, A243, A242, NAGATA_1:def 7; :: thesis:

end;

end;

end;

A244: S₁₀[ 0 ] ;
for n being Element of NAT holds S₁₀[n] from NAT_1:sch 1(A244, A229);
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A225, A228; :: thesis:

end;

end;

end;

SumFpr = ADD "**" SFpr by A59;
then SumFpr . pr <= (SumFpq . pq) + (SumFrq . rq) by A220, A219, XXREAL_0:2;
hence SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) by A218, NAGATA_1:def 8; :: thesis:

end;

end;

then A245: SumFTS is_a_pseudometric_of the carrier of T by NAGATA_1:28;
A246: 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:] )

let p be Point of T; :: thesis:
let fd be Element of Funcs ( the carrier of T,REAL); :: thesis:
reconsider FD = Fdist . fd as RealMap of [:T,T:] by FUNCT_2:66;
assume fd in H₃(p) ; :: thesis:
then consider A being Subset of T such that
A247: fd = Fn . A and
A248: A in Bn . n and
A in H₂(Sx . p) ;
A249: S₄[fd,Fdist . fd] by A42;
S₆[A,Fn . A] by A24, A248;
then FD is continuous by A247, A249, NAGATA_1:21;
hence ( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) by A42; :: thesis:

end;

A250: for pq9 being Point of [:T,T:] holds SumFdist . pq9 is continuous RealMap of [:T,T:]

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

let n be Element of NAT ; :: thesis:
assume that
A252: 0 <> n and
A253: n <= len SF ; :: thesis:
n >= 1 by A252, NAT_1:14;
then n in dom SF by A253, FINSEQ_3:25;
then SF . n in H₄(H₃(p) \/ H₃(q)) by A251, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A254: SF . n = Fdist . fd and
A255: fd in H₃(p) \/ H₃(q) ;
A256: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
( fd in H₃(p) or fd in H₃(q) ) by A255, XBOOLE_0:def 3;
hence SF . n is continuous RealMap of [:T,T:] by A246, A254, A256; :: thesis:

end;

then ADD "**" SF is continuous RealMap of [:T,T:] by A60, NAGATA_1:25;
hence SumFdist . pq9 is continuous RealMap of [:T,T:] by A59; :: thesis:

end;

A257: for pq9 being Point of [:T,T:] holds SumFdist9 . pq9 is continuous Function of [:T,T:],R^1

let pq9 be Point of [:T,T:]; :: thesis:
reconsider SF = SumFdist . pq9 as Function of [:T,T:],R^1 by A250, TOPMETR:17;
SumFdist . pq9 is continuous RealMap of [:T,T:] by A250;
then SF is continuous by TOPREAL6:74;
hence SumFdist9 . pq9 is continuous Function of [:T,T:],R^1 ; :: thesis:

end;

take min (1,SumFTS9) ; :: thesis:
A258: for p, q being Point of T holds (min (1,SumFTS9)) . [p,q] <= 1

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

end;

for p, q being Point of [:T,T:] st p in SS . q holds
(SumFdist9 . p) . p = (SumFdist9 . q) . p by A112;
then SumFdist9 Toler is continuous by A257, A32, NAGATA_1:26;
then SumFTS9 is continuous by TOPREAL6:74;
then ( min (1,SumFTS9) = min (1,SumFTS) & min (1,SumFTS9) is continuous ) by BORSUK_1:def 2, NAGATA_1:27;
hence S₁[n,m, min (1,SumFTS9)] by A245, A258, A109, NAGATA_1:30; :: thesis:

end;

A259: 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] )

A260: NAT = rng PairFunc by Th2, FUNCT_2:def 3;
let k be set ; :: thesis:
assume k in NAT ; :: thesis:
then consider nm being set such that
A261: nm in dom PairFunc and
A262: k = PairFunc . nm by A260, FUNCT_1:def 3;
consider n, m being set such that
A263: ( n in NAT & m in NAT ) and
A264: nm = [n,m] by A261, ZFMISC_1:def 2;
consider pmet9 being RealMap of [:T,T:] such that
A265: S₁[n,m,pmet9] by A7, A263;
take pmet9 ; :: thesis:
thus pmet9 in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8; :: thesis:
take pm = pmet9; :: thesis:
thus pm = pmet9 ; :: thesis:
let n1, m1 be Element of NAT ; :: thesis:
assume (PairFunc ") . k = [n1,m1] ; :: thesis:
then [n1,m1] = [n,m] by A261, A262, A264, Lm2, Th2, FUNCT_1:32;
then ( n1 = n & m1 = m ) by ZFMISC_1:27;
hence S₁[n1,m1,pm] by A265; :: thesis:

end;

consider F being Function of NAT,(Funcs ( the carrier of [:T,T:],REAL)) such that
A266: for n being set st n in NAT holds
S₂[n,F . n] from FUNCT_2:sch 1(A259);

A267: now

let n be Element of NAT ; :: thesis:
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;
hence F . n is PartFunc of [: the carrier of T, the carrier of T:],REAL by FUNCT_2:66; :: thesis:

end;

dom F = NAT by FUNCT_2:def 1;
then reconsider F9 = F as Functional_Sequence of [: the carrier of T, the carrier of T:],REAL by A267, SEQFUNC:1;
A268: for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 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 F9 . k = pmet holds
(lower_bound (pmet,A9)) . p > 0

let p be Point of T; :: thesis:
let A9 be non empty Subset of T; :: thesis:
assume that
A269: not p in A9 and
A270: A9 is closed ; :: thesis:
set O = A9 ` ;
p in A9 ` by A269, XBOOLE_0:def 5;
then consider U being Subset of T such that
A271: p in U and
A272: Cl U c= A9 ` and
A273: U in Union Bn by A1, A5, A270, NAGATA_1:19;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider U = U as open Subset of T by A273, PRE_TOPC:def 2;
consider n being Element of NAT such that
A274: U in Bn . n by A273, PROB_1:12;
consider W being Subset of T such that
A275: ( p in W & Cl W c= U ) and
A276: W in Union Bn by A1, A5, A271, NAGATA_1:19;
Union Bn c= the topology of T by A5, TOPS_2:64;
then reconsider W = W as open Subset of T by A276, PRE_TOPC:def 2;
consider m being Element of NAT such that
A277: W in Bn . m by A276, PROB_1:12;
set k = PairFunc . [n,m];
consider G being RealMap of [:T,T:] such that
A278: G = F . (PairFunc . [n,m]) and
A279: for n, m being Element of NAT st (PairFunc ") . (PairFunc . [n,m]) = [n,m] holds
S₁[n,m,G] by A266;
dom PairFunc = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m] = (PairFunc ") . (PairFunc . [n,m]) by Lm2, Th2, FUNCT_1:32;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A280: G = pmet and
G is continuous and
pmet is_a_pseudometric_of the carrier of T and
A281: 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 A279;
A282: for rn being real number st rn in (dist (pmet,p)) .: A9 holds
rn >= 1

let rn be real number ; :: thesis:
assume rn in (dist (pmet,p)) .: A9 ; :: thesis:
then consider a being set such that
A283: a in dom (dist (pmet,p)) and
A284: a in A9 and
A285: rn = (dist (pmet,p)) . a by FUNCT_1:def 6;
reconsider a = a as Point of T by A283;
A286: pmet . (p,a) = (dist (pmet,p)) . a by Def2;
U c= Cl U by PRE_TOPC:18;
then U c= A9 ` by A272, XBOOLE_1:1;
then U misses A9 by SUBSET_1:23;
then not a in U by A284, XBOOLE_0:3;
hence rn >= 1 by A275, A274, A277, A281, A285, A286; :: thesis:

end;

take PairFunc . [n,m] ; :: thesis:
the carrier of T = dom (dist (pmet,p)) by FUNCT_2:def 1;
then lower_bound ((dist (pmet,p)) .: A9) >= 1 by A282, SEQ_4:43;
hence for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . (PairFunc . [n,m]) = pmet holds
(lower_bound (pmet,A9)) . p > 0 by A278, A280, Def3; :: thesis:

end;

for k being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( F9 . 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 pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )

let k be Element of NAT ; :: thesis:
consider Fk being RealMap of [:T,T:] such that
A287: Fk = F . k and
A288: for n, m being Element of NAT st (PairFunc ") . k = [n,m] holds
S₁[n,m,Fk] by A266;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being set such that
A289: nm in dom PairFunc and
A290: k = PairFunc . nm by FUNCT_1:def 3;
consider n, m being set such that
A291: ( n in NAT & m in NAT ) and
A292: nm = [n,m] by A289, ZFMISC_1:def 2;
[n,m] = (PairFunc ") . k by A289, A290, A292, Lm2, Th2, FUNCT_1:32;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A293: Fk = pmet and
A294: Fk is continuous and
A295: pmet is_a_pseudometric_of the carrier of T and
A296: 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 A291, A288;
take pmet ; :: thesis:
thus ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A287, A293, A295; :: thesis:
thus for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 :: thesis:

let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis:
ex p, q being set st
( p in the carrier of T & q in the carrier of T & pq = [p,q] ) by ZFMISC_1:def 2;
hence pmet . pq <= 1 by A296; :: thesis:

end;

thus for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous by A293, A294; :: thesis:

end;

hence T is metrizable by A2, A268, Th17; :: thesis:

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: