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₁[ object , object , 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₂[ object , object ] means ex F being RealMap of [:T,T:] st
( F = $2 & ( for n, m being 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 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) = |.(($1 . p) - ($1 . q)).|;
let n, m be Nat; :: thesis:
deffunc H₁( object ) -> set = union { Q where Q is Subset of T : ex D1 being set st
( D1 = $1 & Q in Bn . m & Cl Q c= D1 ) } ;
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 object st A in bool the carrier of T holds
H₁(A) in bool the carrier of T

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

let uv be object ; :: 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 : ex D1 being set st
( D1 = A & Q in Bn . m & Cl Q c= D1 ) } by TARSKI:def 4;
ex B being Subset of T st
( v = B & ex D1 being set st
( D1 = A & B in Bn . m & Cl B c= D1 ) ) by A10;
hence uv in the carrier of T by A9; :: thesis:

end;

then H₁(A) c= the carrier of T ;
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 object st A in bool the carrier of T holds
Vm . A = H₁(A) from FUNCT_2:sch 2(A8);
defpred S₆[ object , object ] 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: m in NAT by ORDINAL1:def 12;
A13: Bn . m is locally_finite by A6, NAGATA_1:def 3, A12;
A14: 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 : ex D1 being set st
( D1 = A & Q in Bn . m & Cl Q c= D1 ) } ;
{ Q where Q is Subset of T : ex D1 being set st
( D1 = A & Q in Bn . m & Cl Q c= D1 ) } c= bool the carrier of T

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

end;

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

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

end;

VmA c= Bn . m

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

end;

then A20: Cl (union VmA) = union (clf VmA) by A13, PCOMPS_1:9, PCOMPS_1:20;
Vm . A = H₁(A) by A11;
hence Cl (Vm . A) c= A by A15, A20; :: thesis:

end;

A21: for A being object st A in Bn . n holds
ex f being object st
( f in Funcs ( the carrier of T,REAL) & S₆[A,f] )

let A be object ; :: thesis:
assume A in Bn . n ; :: thesis:
then A22: 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 A22, PRE_TOPC:def 2;
A ` misses A by XBOOLE_1:79;
then A23: A ` misses Cl (Vm . A) by A14, XBOOLE_1:63;
T is normal by A1, A4, NAGATA_1:20;
then consider f being Function of T,R^1 such that
A24: ( 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 A23, URYSOHN3:20;
reconsider f9 = f as RealMap of T by TOPMETR:17;
A25: 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 A24, JORDAN5A:27; :: thesis:

end;

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

end;

consider Fn being Function of (Bn . n),(Funcs ( the carrier of T,REAL)) such that
A26: for A being object st A in Bn . n holds
S₆[A,Fn . A] from FUNCT_2:sch 1(A21);
A27: n in NAT by ORDINAL1:def 12;
Bn . n is locally_finite by A6, NAGATA_1:def 3, A27;
then A28: 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
A29: for p being Element of the carrier of T holds S₅[p,Sx . p] from FUNCT_2:sch 3(A28);
defpred S₇[ object , object ] means for x, y being Element of T st $1 = [x,y] holds
$2 = [:(Sx . x),(Sx . y):];
A30: for pq9 being object st pq9 in the carrier of [:T,T:] holds
ex SS being object st
( SS in bool the carrier of [:T,T:] & S₇[pq9,SS] )

let pq9 be object ; :: 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 object such that
A31: ( p in the carrier of T & q in the carrier of T ) and
A32: pq9 = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A31;

let p1, q1 be Point of T; :: thesis:
assume A33: pq9 = [p1,q1] ; :: thesis:
then p1 = p by A32, XTUPLE_0:1;
hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] by A32, A33, XTUPLE_0:1; :: thesis:

end;

hence ex SS being object 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
A34: for pq being object st pq in the carrier of [:T,T:] holds
S₇[pq,SS . pq] from FUNCT_2:sch 1(A30);
A35: 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 object such that
A36: ( p in the carrier of T & q in the carrier of T ) and
A37: pq9 = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A36;
A38: ( p in Sx . p & q in Sx . q ) by A29;
A39: ( Sx . p is open & Sx . q is open ) by A29;
SS . pq9 = [:(Sx . p),(Sx . q):] by A34, A37;
hence ( pq9 in SS . pq9 & SS . pq9 is open ) by A37, A38, A39, BORSUK_1:6, ZFMISC_1:def 2; :: thesis:

end;

A40: 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
A41: 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(A40);
A42: 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, object ] means $3 = |.((f . $1) - (f . $2)).|;
A43: for x, y being Element of the carrier of T ex r being Element of REAL st S₈[x,y,r]

let x, y be Element of the carrier of T; :: thesis:
consider r being Real such that
A44: S₈[x,y,r] ;
reconsider r = r as Element of REAL by XREAL_0:def 1;
S₈[x,y,r] by A44;
hence ex r being Element of REAL st S₈[x,y,r] ; :: thesis:

end;

consider Fd being Function of [: the carrier of T, the carrier of T:],REAL such that
A45: for x, y being Element of the carrier of T holds S₈[x,y,Fd . (x,y)] from BINOP_1:sch 3(A43);
[: 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 A45; :: thesis:

end;

consider Fdist being Function of (Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)) such that
A46: for fd being Element of Funcs ( the carrier of T,REAL) holds S₄[fd,Fdist . fd] from FUNCT_2:sch 3(A42);
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)) ) );
A47: 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) } ;
A48: H₃(p) c= { H₅(A) where A is Subset of T : A in H₂(Sx . p) }

let FA be object ; :: 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;

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

end;

A50: 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:
A51: H₄(H₃(p) \/ H₃(q)) c= Funcs ( the carrier of [:T,T:],REAL)

let FDm be object ; :: according to TARSKI:def 3 :: thesis:
assume FDm in H₄(H₃(p) \/ H₃(q)) ; :: thesis:
then consider fd being RealMap of T such that
A52: 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 A52, 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) } ;
A53: 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 object ; :: according to TARSKI:def 3 :: thesis:
assume Fdistfd in H₄(H₃(p) \/ H₃(q)) ; :: thesis:
then consider fd being RealMap of T such that
A54: ( 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 A54; :: thesis:

end;

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

end;

A56: 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 object such that
A57: ( p in the carrier of T & q in the carrier of T ) and
A58: pq = [p,q] by ZFMISC_1:def 2;
reconsider p = p, q = q as Point of T by A57;
consider SF being FinSequence such that
A59: rng SF = H₄(H₃(p) \/ H₃(q)) and
A60: SF is one-to-one by A50, FINSEQ_4:58;
rng SF c= Funcs ( the carrier of [:T,T:],REAL) by A50, A59;
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 A58, A59, A60; :: thesis:

end;

consider SFdist being Function of the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *) such that
A61: for pq being Element of the carrier of [:T,T:] holds S₈[pq,SFdist . pq] from FUNCT_2:sch 3(A56);
defpred S₉[ object , object ] means for FS being FinSequence of Funcs ( the carrier of [:T,T:],REAL) st FS = SFdist . $1 holds
$2 = ADD "**" FS;
A62: for pq being object st pq in the carrier of [:T,T:] holds
ex S being object st
( S in Funcs ( the carrier of [:T,T:],REAL) & S₉[pq,S] )

let pq be object ; :: 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 object 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
A63: for xy being object st xy in the carrier of [:T,T:] holds
S₉[xy,SumFdist . xy] from FUNCT_2:sch 1(A62);
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;
A64: 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 A41;
hence ADD . (f1,f2) = f1 + f2 ; :: thesis:

end;

A65: 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
A66: A in Bn . m and
A67: B in Bn . n and
A68: p in A and
A69: Cl A c= B and
A70: not q in B ;
A71: S₆[B,Fn . B] by A26, A67;
A in { Q where Q is Subset of T : ex D1 being set st
( D1 = B & Q in Bn . m & Cl Q c= D1 ) } by A66, A69;
then A c= H₁(B) by ZFMISC_1:74;
then A72: A c= Vm . B by A11;
Vm . B c= Cl (Vm . B) by PRE_TOPC:18;
then A73: p in Cl (Vm . B) by A68, A72;
( Cl (Vm . B) c= B & p in Sx . p ) by A14, A29;
then Sx . p meets B by A73, XBOOLE_0:3;
then A74: B in H₂(Sx . p) by A67;
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
A75: [x,y] = pq and
A76: rng SF = H₄(H₃(x) \/ H₃(y)) by A61;
reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:66;
assume A77: SumFTS9 . [p,q] < 1 ; :: thesis:
reconsider FnB = Fn . B as RealMap of T by A67, FUNCT_2:5, FUNCT_2:66;
A78: FnB in Funcs ( the carrier of T,REAL) by A67, FUNCT_2:5;
q in B ` by A70, XBOOLE_0:def 5;
then A79: FnB . q = 0 by A71;
x = p by A75, XTUPLE_0:1;
then FnB in H₃(x) by A67, A74;
then FnB in H₃(x) \/ H₃(y) by XBOOLE_0:def 3;
then A80: Fdist . FnB in rng SF by A76;
then reconsider FdistFnB = Fdist . FnB as RealMap of [:T,T:] by FUNCT_2:66;
SF <> {} by A80, RELAT_1:38;
then len SF >= 1 by NAT_1:14;
then consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A81: F . 1 = SF . 1 and
A82: for n being Nat st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A83: ADD "**" SF = F . (len SF) by FINSOP_1:def 1;
A84: ( SumFTS . pq = (SumFdist . pq) . pq & SumFdist . pq = ASF ) by A63, NAGATA_1:def 8;
defpred S₁₀[ Nat] means for k being 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;
A85: for k being 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 Nat; :: thesis:
assume that
A86: k <> 0 and
A87: k <= len SF ; :: thesis:
k >= 1 by A86, NAT_1:14;
then k in dom SF by A87, FINSEQ_3:25;
then SF . k in H₄(H₃(x) \/ H₃(y)) by A76, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A88: Fdist . fd = SF . k and
fd in H₃(x) \/ H₃(y) ;
let f be RealMap of [:T,T:]; :: thesis:
assume A89: f = SF . k ; :: thesis:
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then f . (p,q) = |.((fd . p) - (fd . q)).| by A46, A89, A88;
hence f . pq >= 0 by COMPLEX1:46; :: thesis:

end;

A90: for i being Nat st S₁₀[i] holds
S₁₀[i + 1]

let i be Nat; :: thesis:
assume A91: S₁₀[i] ; :: thesis:
let k be Nat; :: thesis:
assume that
A92: k <> 0 and
A93: k <= i + 1 and
A94: i + 1 <= len SF ; :: thesis:

1 <= i + 1 by NAT_1:14;
then i + 1 in dom SF by A94, 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
A95: fk = SF . k and
A96: Fn = F . (i + 1) ; :: thesis:

per cases by A93, XXREAL_0:1;

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

A98: i < len SF by A94, NAT_1:13;
i <> 0 by A92, A97, NAT_1:13;
then F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A82, A98;
then A99: Fn = Fi + SFi1 by A64, A96;
SFi1 . pq >= 0 by A85, A94;
then (Fi . pq) + 0 <= (Fi . pq) + (SFi1 . pq) by XREAL_1:7;
then A100: Fn . pq >= Fi . pq by A99, NAGATA_1:def 7;
A101: i <= len SF by A94, NAT_1:13;
k <= i by A97, NAT_1:13;
then fk . pq <= Fi . pq by A91, A92, A95, A101;
hence fk . pq <= Fn . pq by A100, XXREAL_0:2; :: thesis:

end;

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

suppose i = 0 ; :: thesis:

hence fk . pq <= Fn . pq by A81, A95, A96, A102; :: thesis:

end;

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

i + 0 < i + 1 by XREAL_1:8;
then A104: i < len SF by A94, XXREAL_0:2;
1 <= i by A103, NAT_1:14;
then i in dom SF by A104, 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 A85, A103, A104;
then 0 <= Fi . pq by A91, A103, A104;
then A105: (Fi . pq) + (fk . pq) >= 0 + (fk . pq) by XREAL_1:7;
F . (i + 1) = ADD . ((F . i),(SF . (i + 1))) by A82, A103, A104;
then Fn = Fi + fk by A64, A95, A96, A102;
hence fk . pq <= Fn . pq by A105, 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;

A106: S₁₀[ 0 ] ;
A107: for i being Nat holds S₁₀[i] from NAT_1:sch 2(A106, A90);
consider k being object such that
A108: k in dom SF and
A109: SF . k = Fdist . FnB by A80, FUNCT_1:def 3;
A110: k in Seg (len SF) by A108, FINSEQ_1:def 3;
FnB . p = 1 by A73, A71;
then A111: FdistFnB . (p,q) = |.(1 - 0).| by A46, A78, A79;
reconsider k = k as Element of NAT by A108;
A112: |.1.| = 1 by ABSVALUE:def 1;
( k <> 0 & k <= len SF ) by A110, FINSEQ_1:1;
hence contradiction by A77, A84, A83, A107, A111, A112, A109; :: thesis:

end;

A113: now :: thesis:

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 A65;
then A114: 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 (jj,SumFTS9)) . [p,q] by A114, NAGATA_1:def 9; :: thesis:

end;

A115: 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 A41;
then (map9 . pq) + (map9 . pq) = map9 . pq by NAGATA_1:def 7;
hence map9 . pq = 0 ; :: thesis:

end;

A116: 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
A117: [p1,q1] = pq1 and
A118: rng S1 = H₄(H₃(p1) \/ H₃(q1)) by A61;
A119: 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 A120: [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 A34;
then A121: ( p in Sx . p1 & q in Sx . q1 ) by A120, ZFMISC_1:87;
let no0 be object ; :: according to TARSKI:def 3 :: thesis:
assume no0 in H₅(p,q) ; :: thesis:
then consider A being Subset of T such that
A122: no0 = Fn . A and
A123: A in Bn . n and
A124: 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 A123, FUNCT_2:5, FUNCT_2:66;
A125: ( FnA . p > 0 or FnA . q > 0 ) by A124;
S₆[A,Fn . A] by A26, A123;
then ( not p in the carrier of T \ A or not q in the carrier of T \ A ) by A125;
then ( p in A or q in A ) by XBOOLE_0:def 5;
then ( A meets Sx . p1 or A meets Sx . q1 ) by A121, XBOOLE_0:3;
then ( A in H₂(Sx . p1) or A in H₂(Sx . q1) ) by A123;
then ( FnA in H₃(p1) or FnA in H₃(q1) ) by A123;
hence no0 in H₃(p1) \/ H₃(q1) by A122, XBOOLE_0:def 3; :: thesis:

end;

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

( p1 in Sx . p1 & q1 in Sx . q1 ) by A29;
then [p1,q1] in [:(Sx . p1),(Sx . q1):] by ZFMISC_1:87;
then [p1,q1] in SS . [p1,q1] by A34;
then A127: H₅(p1,q1) c= H₃(p1) \/ H₃(q1) by A119;
let FD be object ; :: 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 A127; :: thesis:

end;

A128: 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 A129: 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 A130: len f = 0 ; :: thesis:

A131: ADD is having_a_unity by A64, NAGATA_1:23;
then A132: 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 A130, A131, FINSOP_1:def 1;
then ADD "**" f is_a_unity_wrt ADD by A132, BINOP_1:def 8;
hence (ADD "**" f) . pq = 0 by A115; :: thesis:

end;

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

then len f >= 1 by NAT_1:14;
then consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A134: F . 1 = f . 1 and
A135: for n being Nat st 0 <> n & n < len f holds
F . (n + 1) = ADD . ((F . n),(f . (n + 1))) and
A136: ADD "**" f = F . (len f) by FINSOP_1:def 1;
defpred S₁₀[ Nat] means ( $1 <> 0 & $1 <= len f implies (F . $1) . pq = 0 );
A137: for k being Nat st S₁₀[k] holds
S₁₀[k + 1]

let k be Nat; :: thesis:
assume A138: S₁₀[k] ; :: thesis:
assume that
k + 1 <> 0 and
A139: k + 1 <= len f ; :: thesis:
A140: k < len f by A139, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom f by A139, FINSEQ_3:25;
then A141: f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) \ H₄(H₅(p,q)) by A129, FUNCT_1:def 3;
then f . (k + 1) in H₄(H₃(p1) \/ H₃(q1)) ;
then consider fd being RealMap of T such that
A142: Fdist . fd = f . (k + 1) and
A143: 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 A142, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A144: Fdistfd . (p,q) = |.((fd . p) - (fd . q)).| by A46;
A145: not f . (k + 1) in H₄(H₅(p,q)) by A141, XBOOLE_0:def 5;
A146: ( fd . p = 0 & fd . q = 0 )

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

per cases by A143, XBOOLE_0:def 3;

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

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

end;

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

then consider A being Subset of T such that
A151: fd = Fn . A and
A152: A in Bn . n and
A in H₂(Sx . q1) ;
A153: S₆[A,Fn . A] by A26, A152;
not fd in H₅(p,q) by A145, A142;
then ex FnA being RealMap of T st
( Fn . A = FnA & not FnA . p > 0 & not FnA . q > 0 ) by A151, A152;
hence contradiction by A147, A151, A153; :: thesis:

end;

end;

end;

suppose k = 0 ; :: thesis:

hence (F . (k + 1)) . pq = 0 by A134, A142, A146, A144, ABSVALUE:2; :: thesis:

end;

suppose A154: k > 0 ; :: thesis:

then Fk1 = ADD . (Fk,fk1) by A135, A140;
then Fk1 = Fk + fk1 by A64;
then Fk1 . pq = 0 + (fk1 . pq) by A138, A139, A154, NAGATA_1:def 7, NAT_1:13;
hence (F . (k + 1)) . pq = 0 by A142, A146, A144, ABSVALUE:2; :: thesis:

end;

end;

end;

A155: S₁₀[ 0 ] ;
for n being Nat holds S₁₀[n] from NAT_1:sch 2(A155, A137);
hence (ADD "**" f) . pq = 0 by A133, A136; :: thesis:

end;

end;

end;

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

end;

A156: H₄(H₃(p1) \/ H₃(q1)) is finite by A50;
then consider No being FinSequence such that
A157: rng No = H₄(H₅(p1,q1)) and
A158: No is one-to-one by A126, FINSEQ_4:58;
H₄(H₃(p1) \/ H₃(q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A50;
then A159: H₄(H₅(p1,q1)) c= Funcs ( the carrier of [:T,T:],REAL) by A126;
then reconsider No = No as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A157, FINSEQ_1:def 4;
consider p2, q2 being Point of T such that
A160: [p2,q2] = pq2 and
A161: rng S2 = H₄(H₃(p2) \/ H₃(q2)) by A61;
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));
A162: S2 is one-to-one by A61;
A163: ( ADD is having_a_unity & ADD is commutative & ADD is associative ) by A64, NAGATA_1:23;
S1 is one-to-one by A61;
then consider S1No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S1No is one-to-one and
A164: rng S1No = (rng S1) \ (rng No) and
A165: ADD "**" S1 = ADD . ((ADD "**" No),(ADD "**" S1No)) by A118, A126, A157, A158, A163, Th18;
consider NoiS2 being FinSequence such that
A166: rng NoiS2 = H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) and
A167: NoiS2 is one-to-one by A126, A156, 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 A159;
then reconsider NoiS2 = NoiS2 as FinSequence of Funcs ( the carrier of [:T,T:],REAL) by A166, FINSEQ_1:def 4;
rng NoiS2 c= rng No by A157, A166, XBOOLE_1:17;
then consider NoNoiS2 being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
NoNoiS2 is one-to-one and
A168: rng NoNoiS2 = (rng No) \ (rng NoiS2) and
A169: ADD "**" No = ADD . ((ADD "**" NoiS2),(ADD "**" NoNoiS2)) by A158, A163, A167, Th18;
rng NoiS2 c= rng S2 by A161, A166, XBOOLE_1:17;
then consider S2No being FinSequence of Funcs ( the carrier of [:T,T:],REAL) such that
S2No is one-to-one and
A170: rng S2No = (rng S2) \ (rng NoiS2) and
A171: ADD "**" S2 = ADD . ((ADD "**" NoiS2),(ADD "**" S2No)) by A163, A167, A162, 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 A161, A166, A170, XBOOLE_1:47;
then A172: AS2No . pq1 = 0 by A128, A117;
ANo = ANoiS2 + ANoNoiS2 by A64, A169;
then A173: ANo . pq1 = (ANoiS2 . pq1) + (ANoNoiS2 . pq1) by NAGATA_1:def 7;
AS1 = ANo + AS1No by A64, A165;
then A174: AS1 . pq1 = (ANo . pq1) + (AS1No . pq1) by NAGATA_1:def 7;
AS2 = ANoiS2 + AS2No by A64, A171;
then A175: AS2 . pq1 = (ANoiS2 . pq1) + (AS2No . pq1) by NAGATA_1:def 7;
A176: AS1No . pq1 = 0 by A128, A117, A118, A157, A164;
thus ( pq1 in SS . pq2 implies (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 ) :: thesis:

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

let FD be object ; :: thesis:
assume FD in H₄(H₅(p1,q1)) ; :: thesis:
then A180: ex fd being RealMap of T st
( FD = Fdist . fd & fd in H₅(p1,q1) ) ;
H₅(p1,q1) c= H₃(p2) \/ H₃(q2) by A119, A117, A160, A179;
hence FD in H₄(H₃(p2) \/ H₃(q2)) by A180; :: thesis:

end;

then H₄(H₅(p1,q1)) c= H₄(H₃(p2) \/ H₃(q2)) ;
then H₄(H₅(p1,q1)) /\ H₄(H₃(p2) \/ H₃(q2)) = H₄(H₅(p1,q1)) by XBOOLE_1:28;
then rng NoNoiS2 = {} by A157, A166, A168, XBOOLE_1:37;
then NoNoiS2 = {} by RELAT_1:41;
then len NoNoiS2 = 0 ;
then ADD "**" NoNoiS2 = the_unity_wrt ADD by A177, FINSOP_1:def 1;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by A178, BINOP_1:def 8;
then A181: AS1 . pq1 = AS2 . pq1 by A115, A174, A173, A175, A176, A172;
SumFdist . pq1 = AS1 by A63;
hence (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1 by A63, A181; :: thesis:

end;

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

set N = NoNoiS2;

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

A184: ADD is having_a_unity by A64, NAGATA_1:23;
then A185: 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 A183, A184, FINSOP_1:def 1;
then ADD "**" NoNoiS2 is_a_unity_wrt ADD by A185, BINOP_1:def 8;
hence ANoNoiS2 . (p1,q1) >= 0 by A115, A117; :: thesis:

end;

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

then len NoNoiS2 >= 1 by NAT_1:14;
then consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A187: F . 1 = NoNoiS2 . 1 and
A188: for n being Nat st 0 <> n & n < len NoNoiS2 holds
F . (n + 1) = ADD . ((F . n),(NoNoiS2 . (n + 1))) and
A189: ADD "**" NoNoiS2 = F . (len NoNoiS2) by FINSOP_1:def 1;
defpred S₁₀[ Nat] means ( $1 <> 0 & $1 <= len NoNoiS2 implies for Fn being RealMap of [:T,T:] st Fn = F . $1 holds
Fn . (p1,q1) >= 0 );
A190: for k being Nat st S₁₀[k] holds
S₁₀[k + 1]

let k be Nat; :: thesis:
assume A191: S₁₀[k] ; :: thesis:
assume that
k + 1 <> 0 and
A192: k + 1 <= len NoNoiS2 ; :: thesis:
A193: k < len NoNoiS2 by A192, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom NoNoiS2 by A192, FINSEQ_3:25;
then NoNoiS2 . (k + 1) in (rng No) \ (rng NoiS2) by A168, FUNCT_1:def 3;
then NoNoiS2 . (k + 1) in H₄(H₅(p1,q1)) by A157, XBOOLE_0:def 5;
then consider fd being RealMap of T such that
A194: 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 A194, FUNCT_2:5, FUNCT_2:66;
A195: |.((fd . p1) - (fd . q1)).| >= 0 by COMPLEX1:46;
A196: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A197: Fdistfd . (p1,q1) = |.((fd . p1) - (fd . q1)).| by A46;

A198: now :: thesis:

suppose k = 0 ; :: thesis:

hence Fk1 . (p1,q1) >= 0 by A46, A187, A194, A196, A195; :: thesis:

end;

suppose A199: k > 0 ; :: thesis:

Fk1 = ADD . (Fk,Nk1) by A188, A193, A199;
then A200: Fk1 = Fk + Nk1 by A64;
Fk . (p1,q1) >= 0 by A191, A192, A199, NAT_1:13;
then 0 + 0 <= (Fk . (p1,q1)) + (Nk1 . (p1,q1)) by A194, A195, A197;
hence Fk1 . (p1,q1) >= 0 by A117, A200, 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 A198; :: thesis:

end;

A201: S₁₀[ 0 ] ;
for n being Nat holds S₁₀[n] from NAT_1:sch 2(A201, A190);
hence ANoNoiS2 . (p1,q1) >= 0 by A186, A189; :: thesis:

end;

end;

end;

A202: AS2 . (p1,q1) <= AS1 . (p1,q1) by A117, A182, A174, A173, A175, A176, A172, XREAL_1:7;
let SumFdist1, SumFdist2 be RealMap of [:T,T:]; :: thesis:
assume that
A203: SumFdist1 = SumFdist . pq1 and
A204: SumFdist2 = SumFdist . pq2 ; :: thesis:
SumFdist2 = AS2 by A63, A204;
hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A63, A117, A203, A202; :: 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;

A205: now :: thesis:

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

A207: ADD is having_a_unity by A64, NAGATA_1:23;
then A208: 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 A206, A207, FINSOP_1:def 1;
then ADD "**" SF is_a_unity_wrt ADD by A208, BINOP_1:def 8;
hence (ADD "**" SF) . pp = 0 by A115; :: thesis:

end;

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

then len SF >= 1 by NAT_1:14;
then consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A210: F . 1 = SF . 1 and
A211: for n being Nat st 0 <> n & n < len SF holds
F . (n + 1) = ADD . ((F . n),(SF . (n + 1))) and
A212: ADD "**" SF = F . (len SF) by FINSOP_1:def 1;
defpred S₁₀[ Nat] means ( $1 <> 0 & $1 <= len SF implies (F . $1) . pp = 0 );
A213: for k being Nat st S₁₀[k] holds
S₁₀[k + 1]

let k be Nat; :: thesis:
assume A214: S₁₀[k] ; :: thesis:
consider x, y being Point of T such that
[x,y] = pp and
A215: rng SF = H₄(H₃(x) \/ H₃(y)) by A61;
assume that
k + 1 <> 0 and
A216: k + 1 <= len SF ; :: thesis:
A217: k < len SF by A216, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SF by A216, FINSEQ_3:25;
then SF . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A215, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A218: 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 A218, FUNCT_2:5, FUNCT_2:66;
fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A219: Fdistfd . (p,p) = |.((fd . p) - (fd . p)).| by A46;

suppose k = 0 ; :: thesis:

hence (F . (k + 1)) . pp = 0 by A210, A218, A219, ABSVALUE:2; :: thesis:

end;

suppose A220: k > 0 ; :: thesis:

Fk1 = ADD . (Fk,SFk1) by A211, A217, A220;
then Fk1 = Fk + SFk1 by A64;
then Fk1 . pp = 0 + (SFk1 . pp) by A214, A216, A220, NAGATA_1:def 7, NAT_1:13;
hence (F . (k + 1)) . pp = 0 by A218, A219, ABSVALUE:2; :: thesis:

end;

end;

end;

A221: S₁₀[ 0 ] ;
for n being Nat holds S₁₀[n] from NAT_1:sch 2(A221, A213);
hence (ADD "**" SF) . pp = 0 by A209, A212; :: thesis:

end;

end;

end;

SumFdist . pp = ADD "**" SF by A63;
hence SumFTS . (p,p) = 0 by A205, 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;
A222: ( SumFTS . pr = SumFpr . pr & SumFTS . pq = SumFpq . pq ) by NAGATA_1:def 8;
( SumFpr . pq <= SumFpq . pq & SumFpr . rq <= SumFrq . rq ) by A116;
then A223: (SumFpr . pq) + (SumFpr . rq) <= (SumFpq . pq) + (SumFrq . rq) by XREAL_1:7;

A224: now :: thesis:

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

A226: ADD is having_a_unity by A64, NAGATA_1:23;
then A227: 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 A225, A226, FINSOP_1:def 1;
then A228: ADD "**" SFpr is_a_unity_wrt ADD by A227, BINOP_1:def 8;
then ( ASFpr . pr = 0 & ASFpr . pq = 0 ) by A115;
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A115, A228; :: thesis:

end;

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

then len SFpr >= 1 by NAT_1:14;
then consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A230: F . 1 = SFpr . 1 and
A231: for n being Nat st 0 <> n & n < len SFpr holds
F . (n + 1) = ADD . ((F . n),(SFpr . (n + 1))) and
A232: ADD "**" SFpr = F . (len SFpr) by FINSOP_1:def 1;
defpred S₁₀[ 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) );
A233: for k being Nat st S₁₀[k] holds
S₁₀[k + 1]

let k be Nat; :: thesis:
assume A234: S₁₀[k] ; :: thesis:
consider x, y being Point of T such that
[x,y] = pr and
A235: rng SFpr = H₄(H₃(x) \/ H₃(y)) by A61;
assume that
k + 1 <> 0 and
A236: k + 1 <= len SFpr ; :: thesis:
A237: k < len SFpr by A236, NAT_1:13;
k + 1 >= 1 by NAT_1:14;
then k + 1 in dom SFpr by A236, FINSEQ_3:25;
then SFpr . (k + 1) in H₄(H₃(x) \/ H₃(y)) by A235, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A238: 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 A238, FUNCT_2:5, FUNCT_2:66;
A239: (fd . p) - (fd . r) = ((fd . p) - (fd . q)) + ((fd . q) - (fd . r)) ;
then A240: |.((fd . p) - (fd . r)).| <= |.((fd . p) - (fd . q)).| + |.((fd . q) - (fd . r)).| by COMPLEX1:56;
A241: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
then A242: ( Fdistfd . (p,r) = |.((fd . p) - (fd . r)).| & Fdistfd . (p,q) = |.((fd . p) - (fd . q)).| ) by A46;
A243: ( |.((fd . q) - (fd . r)).| = |.(- ((fd . q) - (fd . r))).| & Fdistfd . (r,q) = |.((fd . r) - (fd . q)).| ) by A46, A241, COMPLEX1:52;
let F9 be RealMap of [:T,T:]; :: thesis:
assume A244: F9 = F . (k + 1) ; :: thesis:

suppose k = 0 ; :: thesis:

hence F9 . pr <= (F9 . pq) + (F9 . rq) by A230, A238, A239, A242, A243, A244, COMPLEX1:56; :: thesis:

end;

suppose A245: k > 0 ; :: thesis:

then Fk . pr <= (Fk . pq) + (Fk . rq) by A234, A236, NAT_1:13;
then A246: (Fk . pr) + (SFk1 . pr) <= ((Fk . pq) + (Fk . rq)) + ((SFk1 . pq) + (SFk1 . rq)) by A238, A240, A242, A243, XREAL_1:7;
Fk1 = ADD . (Fk,SFk1) by A231, A237, A245;
then A247: Fk1 = Fk + SFk1 by A64;
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 A244, A247, A246, NAGATA_1:def 7; :: thesis:

end;

end;

end;

A248: S₁₀[ 0 ] ;
for n being Nat holds S₁₀[n] from NAT_1:sch 2(A248, A233);
hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A229, A232; :: thesis:

end;

end;

end;

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

end;

end;

then A249: SumFTS is_a_pseudometric_of the carrier of T by NAGATA_1:28;
A250: 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
A251: fd = Fn . A and
A252: A in Bn . n and
A in H₂(Sx . p) ;
A253: S₄[fd,Fdist . fd] by A46;
S₆[A,Fn . A] by A26, A252;
then FD is continuous by A251, A253, NAGATA_1:21;
hence ( S₄[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) by A46; :: thesis:

end;

A254: 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
A255: rng SF = H₄(H₃(p) \/ H₃(q)) by A61;
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
A256: 0 <> n and
A257: n <= len SF ; :: thesis:
n >= 1 by A256, NAT_1:14;
then n in dom SF by A257, FINSEQ_3:25;
then SF . n in H₄(H₃(p) \/ H₃(q)) by A255, FUNCT_1:def 3;
then consider fd being RealMap of T such that
A258: SF . n = Fdist . fd and
A259: fd in H₃(p) \/ H₃(q) ;
A260: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;
( fd in H₃(p) or fd in H₃(q) ) by A259, XBOOLE_0:def 3;
hence SF . n is continuous RealMap of [:T,T:] by A250, A258, A260; :: thesis:

end;

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

end;

A261: 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 A254, TOPMETR:17;
SumFdist . pq9 is continuous RealMap of [:T,T:] by A254;
then SF is continuous by JORDAN5A:27;
hence SumFdist9 . pq9 is continuous Function of [:T,T:],R^1 ; :: thesis:

end;

take min (jj,SumFTS9) ; :: thesis:
A262: for p, q being Point of T holds (min (jj,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 (jj,SumFTS9)) . [p,q] = min (1,(SumFTS9 . [p,q])) by NAGATA_1:def 9;
hence (min (jj,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 A116;
then SumFdist9 Toler is continuous by A261, A35, NAGATA_1:26;
then SumFTS9 is continuous by JORDAN5A:27;
then ( min (jj,SumFTS9) = min (jj,SumFTS) & min (jj,SumFTS9) is continuous ) by BORSUK_1:def 2, NAGATA_1:27;
hence S₁[n,m, min (jj,SumFTS9)] by A249, A262, A113, NAGATA_1:30; :: thesis:

end;

A263: for k being object st k in NAT holds
ex f being object st
( f in Funcs ( the carrier of [:T,T:],REAL) & S₂[k,f] )

A264: NAT = rng PairFunc by Th2, FUNCT_2:def 3;
let k be object ; :: thesis:
assume k in NAT ; :: thesis:
then consider nm being object such that
A265: nm in dom PairFunc and
A266: k = PairFunc . nm by A264, FUNCT_1:def 3;
consider n, m being object such that
A267: ( n in NAT & m in NAT ) and
A268: nm = [n,m] by A265, ZFMISC_1:def 2;
consider pmet9 being RealMap of [:T,T:] such that
A269: S₁[n,m,pmet9] by A7, A267;
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 Nat; :: thesis:
assume (PairFunc ") . k = [n1,m1] ; :: thesis:
then [n1,m1] = [n,m] by A265, A266, A268, Lm2, Th2, FUNCT_1:32;
then ( n1 = n & m1 = m ) by XTUPLE_0:1;
hence S₁[n1,m1,pm] by A269; :: thesis:

end;

consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A270: for n being object st n in NAT holds
S₂[n,F . n] from FUNCT_2:sch 1(A263);

A271: now :: thesis:

let n be 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 A271, SEQFUNC:1;
A272: 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 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
A273: not p in A9 and
A274: A9 is closed ; :: thesis:
set O = A9 ` ;
p in A9 ` by A273, XBOOLE_0:def 5;
then consider U being Subset of T such that
A275: p in U and
A276: Cl U c= A9 ` and
A277: U in Union Bn by A1, A5, A274, 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 A277, PRE_TOPC:def 2;
consider n being Nat such that
A278: U in Bn . n by A277, PROB_1:12;
consider W being Subset of T such that
A279: ( p in W & Cl W c= U ) and
A280: W in Union Bn by A1, A5, A275, 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 A280, PRE_TOPC:def 2;
consider m being Nat such that
A281: W in Bn . m by A280, PROB_1:12;
set k = PairFunc . [n,m];
A282: PairFunc . [n,m] in NAT by ORDINAL1:def 12;
A283: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
consider G being RealMap of [:T,T:] such that
A284: G = F . (PairFunc . [n,m]) and
A285: for n, m being Nat st (PairFunc ") . (PairFunc . [n,m]) = [n,m] holds
S₁[n,m,G] by A270, A282;
A286: [n,m] in [:NAT,NAT:] by A283, ZFMISC_1:87;
reconsider kk = PairFunc . [n,m] as Element of NAT by ORDINAL1:def 12;
dom PairFunc = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m] = (PairFunc ") . kk by Lm2, Th2, FUNCT_1:32, A286;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A287: G = pmet and
G is continuous and
pmet is_a_pseudometric_of the carrier of T and
A288: 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 A285;
A289: for rn being Real st rn in (dist (pmet,p)) .: A9 holds
rn >= 1

let rn be Real; :: thesis:
assume rn in (dist (pmet,p)) .: A9 ; :: thesis:
then consider a being object such that
A290: a in dom (dist (pmet,p)) and
A291: a in A9 and
A292: rn = (dist (pmet,p)) . a by FUNCT_1:def 6;
reconsider a = a as Point of T by A290;
A293: pmet . (p,a) = (dist (pmet,p)) . a by Def2;
U c= Cl U by PRE_TOPC:18;
then U c= A9 ` by A276;
then U misses A9 by SUBSET_1:23;
then not a in U by A291, XBOOLE_0:3;
hence rn >= 1 by A279, A278, A281, A288, A292, A293; :: 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 A289, 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 A284, A287, Def3; :: thesis:

end;

for k being 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 Nat; :: thesis:
A294: k in NAT by ORDINAL1:def 12;
then consider Fk being RealMap of [:T,T:] such that
A295: Fk = F . k and
A296: for n, m being Nat st (PairFunc ") . k = [n,m] holds
S₁[n,m,Fk] by A270;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being object such that
A297: nm in dom PairFunc and
A298: k = PairFunc . nm by FUNCT_1:def 3, A294;
consider n, m being object such that
A299: ( n in NAT & m in NAT ) and
A300: nm = [n,m] by A297, ZFMISC_1:def 2;
[n,m] = (PairFunc ") . k by A297, A298, A300, Lm2, Th2, FUNCT_1:32;
then consider pmet being Function of [: the carrier of T, the carrier of T:],REAL such that
A301: Fk = pmet and
A302: Fk is continuous and
A303: pmet is_a_pseudometric_of the carrier of T and
A304: 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 A299, A296;
take pmet ; :: thesis:
thus ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A295, A301, A303; :: 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 object 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 A304; :: thesis:

end;

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

end;

hence T is metrizable by A2, A272, 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: