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

thus ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is metrizable ) :: thesis: ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) )

thus ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is metrizable ) :: thesis: ( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) )

proof

thus
( T is metrizable implies ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) )
by NAGATA_1:15, NAGATA_1:16; :: thesis: verum
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: T is metrizable

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_{1}[ 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_{2}[ 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_{1}[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_{1}[n,m,pmet9]

ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S_{2}[k,f] )

A270: for n being object st n in NAT holds

S_{2}[n,F . n]
from FUNCT_2:sch 1(A263);

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

( 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 ) )

end;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: T is metrizable

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

( $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

( F = $2 & ( for n, m being Nat st (PairFunc ") . $1 = [n,m] holds

S

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

proof

A263:
for k being object st k in NAT holds
defpred S_{3}[ 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_{4}[ 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: ex pmet9 being RealMap of [:T,T:] st S_{1}[n,m,pmet9]

deffunc H_{1}( 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_{2}( Subset of T) -> set = { Q where Q is Subset of T : ( Q in Bn . n & Q meets $1 ) } ;

defpred S_{5}[ set , Subset of T] means ( $1 in $2 & $2 is open & H_{2}($2) is finite );

A8: for A being object st A in bool the carrier of T holds

H_{1}(A) in bool the carrier of T

A11: for A being object st A in bool the carrier of T holds

Vm . A = H_{1}(A)
from FUNCT_2:sch 2(A8);

defpred S_{6}[ 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

ex f being object st

( f in Funcs ( the carrier of T,REAL) & S_{6}[A,f] )

A26: for A being object st A in Bn . n holds

S_{6}[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_{5}[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_{5}[p,Sx . p]
from FUNCT_2:sch 3(A28);

defpred S_{7}[ 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_{7}[pq9,SS] )

A34: for pq being object st pq in the carrier of [:T,T:] holds

S_{7}[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 )_{3}[f,g,fg]

A41: for f, g being Element of Funcs ( the carrier of [:T,T:],REAL) holds S_{3}[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_{4}[f,fxy]

A46: for fd being Element of Funcs ( the carrier of T,REAL) holds S_{4}[fd,Fdist . fd]
from FUNCT_2:sch 3(A42);

deffunc H_{3}( Element of T) -> set = { (Fn . A) where A is Subset of T : ( A in Bn . n & A in H_{2}(Sx . $1) ) } ;

deffunc H_{4}( set ) -> set = { (Fdist . fd) where fd is RealMap of T : fd in $1 } ;

defpred S_{8}[ set , Function] means ( $2 is one-to-one & ex p, q being Point of T st

( [p,q] = $1 & rng $2 = H_{4}(H_{3}(p) \/ H_{3}(q)) ) );

A47: for p being Point of T holds H_{3}(p) is finite

( H_{4}(H_{3}(p) \/ H_{3}(q)) is finite & H_{4}(H_{3}(p) \/ H_{3}(q)) c= Funcs ( the carrier of [:T,T:],REAL) )
_{8}[pq,G]

A61: for pq being Element of the carrier of [:T,T:] holds S_{8}[pq,SFdist . pq]
from FUNCT_2:sch 3(A56);

defpred S_{9}[ 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_{9}[pq,S] )

A63: for xy being object st xy in the carrier of [:T,T:] holds

S_{9}[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

( 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

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

map9 . pq = 0

( ( 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 ) )

A250: for p being Point of T

for fd being Element of Funcs ( the carrier of T,REAL) st fd in H_{3}(p) holds

( S_{4}[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
_{1}[n,m, min (jj,SumFTS9)]

A262: for p, q being Point of T holds (min (jj,SumFTS9)) . [p,q] <= 1

(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_{1}[n,m, min (jj,SumFTS9)]
by A249, A262, A113, NAGATA_1:30; :: thesis: verum

end;defpred S

let n, m be Nat; :: thesis: ex pmet9 being RealMap of [:T,T:] st S

deffunc H

( D1 = $1 & Q in Bn . m & Cl Q c= D1 ) } ;

set Bnn = Bn . n;

deffunc H

defpred S

A8: for A being object st A in bool the carrier of T holds

H

proof

consider Vm being Function of (bool the carrier of T),(bool the carrier of T) such that
let A be object ; :: thesis: ( A in bool the carrier of T implies H_{1}(A) in bool the carrier of T )

assume A in bool the carrier of T ; :: thesis: H_{1}(A) in bool the carrier of T

set Um = { Q where Q is Subset of T : ex D1 being set st

( D1 = A & Q in Bn . m & Cl Q c= D1 ) } ;

_{1}(A) c= the carrier of T
;

hence H_{1}(A) in bool the carrier of T
; :: thesis: verum

end;assume A in bool the carrier of T ; :: thesis: H

set Um = { Q where Q is Subset of T : ex D1 being set st

( D1 = A & Q in Bn . m & Cl Q c= D1 ) } ;

now :: thesis: for uv being object st uv in H_{1}(A) holds

uv in the carrier of T

then
Huv in the carrier of T

let uv be object ; :: thesis: ( uv in H_{1}(A) implies uv in the carrier of T )

assume uv in H_{1}(A)
; :: thesis: uv in the carrier of T

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

end;assume uv in H

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

hence H

A11: for A being object st A in bool the carrier of T holds

Vm . A = H

defpred S

( 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

proof

A21:
for A being object st A in Bn . n holds
let A be Subset of T; :: thesis: Cl (Vm . A) c= A

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

( D1 = A & Q in Bn . m & Cl Q c= D1 ) } as Subset-Family of T ;

A15: union (clf VmA) c= A

Vm . A = H_{1}(A)
by A11;

hence Cl (Vm . A) c= A by A15, A20; :: thesis: verum

end;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

proof

then reconsider VmA = { Q where Q is Subset of T : ex D1 being set st
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in { Q where Q is Subset of T : ex D1 being set st

( D1 = A & Q in Bn . m & Cl Q c= D1 ) } or B in bool the carrier of T )

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: B in bool the carrier of T

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

end;( D1 = A & Q in Bn . m & Cl Q c= D1 ) } or B in bool the carrier of T )

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: B in bool the carrier of T

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

( D1 = A & Q in Bn . m & Cl Q c= D1 ) } as Subset-Family of T ;

A15: union (clf VmA) c= A

proof

VmA c= Bn . m
let ClBu be object ; :: according to TARSKI:def 3 :: thesis: ( not ClBu in union (clf VmA) or ClBu in A )

assume ClBu in union (clf VmA) ; :: thesis: ClBu in A

then consider ClB being set such that

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

end;assume ClBu in union (clf VmA) ; :: thesis: ClBu in A

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

proof

then A20:
Cl (union VmA) = union (clf VmA)
by A13, PCOMPS_1:9, PCOMPS_1:20;
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in VmA or B in Bn . m )

assume B in VmA ; :: thesis: B in Bn . m

then ex C being Subset of T st

( B = C & ex D1 being set st

( D1 = A & C in Bn . m & Cl C c= D1 ) ) ;

hence B in Bn . m ; :: thesis: verum

end;assume B in VmA ; :: thesis: B in Bn . m

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

Vm . A = H

hence Cl (Vm . A) c= A by A15, A20; :: thesis: verum

ex f being object st

( f in Funcs ( the carrier of T,REAL) & S

proof

consider Fn being Function of (Bn . n),(Funcs ( the carrier of T,REAL)) such that
let A be object ; :: thesis: ( A in Bn . n implies ex f being object st

( f in Funcs ( the carrier of T,REAL) & S_{6}[A,f] ) )

assume A in Bn . n ; :: thesis: ex f being object st

( f in Funcs ( the carrier of T,REAL) & S_{6}[A,f] )

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

hence ex f being object st

( f in Funcs ( the carrier of T,REAL) & S_{6}[A,f] )
by A25; :: thesis: verum

end;( f in Funcs ( the carrier of T,REAL) & S

assume A in Bn . n ; :: thesis: ex f being object st

( f in Funcs ( the carrier of T,REAL) & S

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

proof

f9 in Funcs ( the carrier of T,REAL)
by FUNCT_2:8;
take
f9
; :: thesis: ex S being Subset of T st

( S = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds

( 0 <= f9 . p & f9 . p <= 1 & ( p in S ` implies f9 . p = 0 ) & ( p in Cl (Vm . S) implies f9 . p = 1 ) ) ) )

take A ; :: thesis: ( 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 ) ) ) )

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

end;( S = A & f9 = f9 & f9 is continuous & ( for p being Point of T holds

( 0 <= f9 . p & f9 . p <= 1 & ( p in S ` implies f9 . p = 0 ) & ( p in Cl (Vm . S) implies f9 . p = 1 ) ) ) )

take A ; :: thesis: ( 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 ) ) ) )

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

hence ex f being object st

( f in Funcs ( the carrier of T,REAL) & S

A26: for A being object st A in Bn . n holds

S

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

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

defpred S

$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

proof

consider SS being Function of the carrier of [:T,T:],(bool the carrier of [:T,T:]) such that
let pq9 be object ; :: thesis: ( pq9 in the carrier of [:T,T:] implies ex SS being object st

( SS in bool the carrier of [:T,T:] & S_{7}[pq9,SS] ) )

assume pq9 in the carrier of [:T,T:] ; :: thesis: ex SS being object st

( SS in bool the carrier of [:T,T:] & S_{7}[pq9,SS] )

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;

( SS in bool the carrier of [:T,T:] & S_{7}[pq9,SS] )
; :: thesis: verum

end;( SS in bool the carrier of [:T,T:] & S

assume pq9 in the carrier of [:T,T:] ; :: thesis: ex SS being object st

( SS in bool the carrier of [:T,T:] & S

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;

now :: thesis: for p1, q1 being Point of T st pq9 = [p1,q1] holds

[:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]

hence
ex SS being object st [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]

let p1, q1 be Point of T; :: thesis: ( pq9 = [p1,q1] implies [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] )

assume A33: pq9 = [p1,q1] ; :: thesis: [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]

then p1 = p by A32, XTUPLE_0:1;

hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] by A32, A33, XTUPLE_0:1; :: thesis: verum

end;assume A33: pq9 = [p1,q1] ; :: thesis: [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):]

then p1 = p by A32, XTUPLE_0:1;

hence [:(Sx . p),(Sx . q):] = [:(Sx . p1),(Sx . q1):] by A32, A33, XTUPLE_0:1; :: thesis: verum

( SS in bool the carrier of [:T,T:] & S

A34: for pq being object st pq in the carrier of [:T,T:] holds

S

A35: for pq9 being Point of [:T,T:] holds

( pq9 in SS . pq9 & SS . pq9 is open )

proof

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
let pq9 be Point of [:T,T:]; :: thesis: ( pq9 in SS . pq9 & SS . pq9 is open )

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

end;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: verum

proof

consider ADD being BinOp of (Funcs ( the carrier of [:T,T:],REAL)) such that
let f, g be Element of Funcs ( the carrier of [:T,T:],REAL); :: thesis: ex fg being Element of Funcs ( the carrier of [:T,T:],REAL) st S_{3}[f,g,fg]

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_{3}[f,g,fg]
; :: thesis: verum

end;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

A41: for f, g being Element of Funcs ( the carrier of [:T,T:],REAL) holds S

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

proof

consider Fdist being Function of (Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)) such that
let f be Element of Funcs ( the carrier of T,REAL); :: thesis: ex fxy being Element of Funcs ( the carrier of [:T,T:],REAL) st S_{4}[f,fxy]

defpred S_{8}[ 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_{8}[x,y,r]

A45: for x, y being Element of the carrier of T holds S_{8}[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_{4}[f,fxy]
by A45; :: thesis: verum

end;defpred S

A43: for x, y being Element of the carrier of T ex r being Element of REAL st S

proof

consider Fd being Function of [: the carrier of T, the carrier of T:],REAL such that
let x, y be Element of the carrier of T; :: thesis: ex r being Element of REAL st S_{8}[x,y,r]

consider r being Real such that

A44: S_{8}[x,y,r]
;

reconsider r = r as Element of REAL by XREAL_0:def 1;

S_{8}[x,y,r]
by A44;

hence ex r being Element of REAL st S_{8}[x,y,r]
; :: thesis: verum

end;consider r being Real such that

A44: S

reconsider r = r as Element of REAL by XREAL_0:def 1;

S

hence ex r being Element of REAL st S

A45: for x, y being Element of the carrier of T holds S

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

A46: for fd being Element of Funcs ( the carrier of T,REAL) holds S

deffunc H

deffunc H

defpred S

( [p,q] = $1 & rng $2 = H

A47: for p being Point of T holds H

proof

A50:
for p, q being Point of T holds
deffunc H_{5}( Subset of T) -> set = Fn . $1;

let p be Point of T; :: thesis: H_{3}(p) is finite

set SFxx = { H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) } ;

A48: H_{3}(p) c= { H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) }
_{2}(Sx . p) is finite
by A29;

{ H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) } is finite
from FRAENKEL:sch 21(A49);

hence H_{3}(p) is finite
by A48; :: thesis: verum

end;let p be Point of T; :: thesis: H

set SFxx = { H

A48: H

proof

A49:
H
let FA be object ; :: according to TARSKI:def 3 :: thesis: ( not FA in H_{3}(p) or FA in { H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) } )

assume FA in H_{3}(p)
; :: thesis: FA in { H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) }

then ex A being Subset of T st

( FA = Fn . A & A in Bn . n & A in H_{2}(Sx . p) )
;

hence FA in { H_{5}(A) where A is Subset of T : A in H_{2}(Sx . p) }
; :: thesis: verum

end;assume FA in H

then ex A being Subset of T st

( FA = Fn . A & A in Bn . n & A in H

hence FA in { H

{ H

hence H

( H

proof

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
deffunc H_{5}( RealMap of T) -> set = Fdist . $1;

let p, q be Point of T; :: thesis: ( H_{4}(H_{3}(p) \/ H_{3}(q)) is finite & H_{4}(H_{3}(p) \/ H_{3}(q)) c= Funcs ( the carrier of [:T,T:],REAL) )

A51: H_{4}(H_{3}(p) \/ H_{3}(q)) c= Funcs ( the carrier of [:T,T:],REAL)
_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) } ;

A53: H_{4}(H_{3}(p) \/ H_{3}(q)) c= { H_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) }
_{3}(p) is finite & H_{3}(q) is finite )
by A47;

then A55: H_{3}(p) \/ H_{3}(q) is finite
;

{ H_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) } is finite
from FRAENKEL:sch 21(A55);

hence ( H_{4}(H_{3}(p) \/ H_{3}(q)) is finite & H_{4}(H_{3}(p) \/ H_{3}(q)) c= Funcs ( the carrier of [:T,T:],REAL) )
by A51, A53; :: thesis: verum

end;let p, q be Point of T; :: thesis: ( H

A51: H

proof

set RNG9 = { H
let FDm be object ; :: according to TARSKI:def 3 :: thesis: ( not FDm in H_{4}(H_{3}(p) \/ H_{3}(q)) or FDm in Funcs ( the carrier of [:T,T:],REAL) )

assume FDm in H_{4}(H_{3}(p) \/ H_{3}(q))
; :: thesis: FDm in Funcs ( the carrier of [:T,T:],REAL)

then consider fd being RealMap of T such that

A52: FDm = Fdist . fd and

fd in H_{3}(p) \/ H_{3}(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: verum

end;assume FDm in H

then consider fd being RealMap of T such that

A52: FDm = Fdist . fd and

fd in H

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

A53: H

proof

( H
let Fdistfd be object ; :: according to TARSKI:def 3 :: thesis: ( not Fdistfd in H_{4}(H_{3}(p) \/ H_{3}(q)) or Fdistfd in { H_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) } )

assume Fdistfd in H_{4}(H_{3}(p) \/ H_{3}(q))
; :: thesis: Fdistfd in { H_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) }

then consider fd being RealMap of T such that

A54: ( Fdistfd = Fdist . fd & fd in H_{3}(p) \/ H_{3}(q) )
;

fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;

hence Fdistfd in { H_{5}(fd) where fd is Element of Funcs ( the carrier of T,REAL) : fd in H_{3}(p) \/ H_{3}(q) }
by A54; :: thesis: verum

end;assume Fdistfd in H

then consider fd being RealMap of T such that

A54: ( Fdistfd = Fdist . fd & fd in H

fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;

hence Fdistfd in { H

then A55: H

{ H

hence ( H

proof

consider SFdist being Function of the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *) such that
let pq be Element of the carrier of [:T,T:]; :: thesis: ex G being Element of (Funcs ( the carrier of [:T,T:],REAL)) * st S_{8}[pq,G]

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_{4}(H_{3}(p) \/ H_{3}(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_{8}[pq,G]
by A58, A59, A60; :: thesis: verum

end;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

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

A61: for pq being Element of the carrier of [:T,T:] holds S

defpred S

$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

proof

consider SumFdist being Function of the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)) such that
let pq be object ; :: thesis: ( pq in the carrier of [:T,T:] implies ex S being object st

( S in Funcs ( the carrier of [:T,T:],REAL) & S_{9}[pq,S] ) )

assume pq in the carrier of [:T,T:] ; :: thesis: ex S being object st

( S in Funcs ( the carrier of [:T,T:],REAL) & S_{9}[pq,S] )

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_{9}[pq,S] )
; :: thesis: verum

end;( S in Funcs ( the carrier of [:T,T:],REAL) & S

assume pq in the carrier of [:T,T:] ; :: thesis: ex S being object st

( S in Funcs ( the carrier of [:T,T:],REAL) & S

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

A63: for xy being object st xy in the carrier of [:T,T:] holds

S

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

proof

A65:
for p, q being Point of T st ex A, B being Subset of T st
let f1, f2 be RealMap of [:T,T:]; :: thesis: ADD . (f1,f2) = f1 + f2

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

end;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: verum

( 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

proof

let p, q be Point of T; :: thesis: ( ex A, B being Subset of T st

( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies SumFTS9 . [p,q] >= 1 )

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

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_{6}[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_{1}(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_{2}(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_{4}(H_{3}(x) \/ H_{3}(y))
by A61;

reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:66;

assume A77: SumFTS9 . [p,q] < 1 ; :: thesis: contradiction

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_{3}(x)
by A67, A74;

then FnB in H_{3}(x) \/ H_{3}(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_{10}[ 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_{10}[i] holds

S_{10}[i + 1]
_{10}[ 0 ]
;

A107: for i being Nat holds S_{10}[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: verum

end;( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies SumFTS9 . [p,q] >= 1 )

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

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

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

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

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

reconsider ASF = ADD "**" SF as RealMap of [:T,T:] by FUNCT_2:66;

assume A77: SumFTS9 . [p,q] < 1 ; :: thesis: contradiction

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

then FnB in H

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

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

proof

A90:
for i being Nat st S
let k be Nat; :: thesis: ( k <> 0 & k <= len SF implies for f being RealMap of [:T,T:] st f = SF . k holds

f . pq >= 0 )

assume that

A86: k <> 0 and

A87: k <= len SF ; :: thesis: for f being RealMap of [:T,T:] st f = SF . k holds

f . pq >= 0

k >= 1 by A86, NAT_1:14;

then k in dom SF by A87, FINSEQ_3:25;

then SF . k in H_{4}(H_{3}(x) \/ H_{3}(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_{3}(x) \/ H_{3}(y)
;

let f be RealMap of [:T,T:]; :: thesis: ( f = SF . k implies f . pq >= 0 )

assume A89: f = SF . k ; :: thesis: f . pq >= 0

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

end;f . pq >= 0 )

assume that

A86: k <> 0 and

A87: k <= len SF ; :: thesis: for f being RealMap of [:T,T:] st f = SF . k holds

f . pq >= 0

k >= 1 by A86, NAT_1:14;

then k in dom SF by A87, FINSEQ_3:25;

then SF . k in H

then consider fd being RealMap of T such that

A88: Fdist . fd = SF . k and

fd in H

let f be RealMap of [:T,T:]; :: thesis: ( f = SF . k implies f . pq >= 0 )

assume A89: f = SF . k ; :: thesis: f . pq >= 0

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

S

proof

A106:
S
let i be Nat; :: thesis: ( S_{10}[i] implies S_{10}[i + 1] )

assume A91: S_{10}[i]
; :: thesis: S_{10}[i + 1]

let k be Nat; :: thesis: ( k <> 0 & k <= i + 1 & i + 1 <= len SF implies for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds

fk . pq <= Fn . pq )

assume that

A92: k <> 0 and

A93: k <= i + 1 and

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

fk . pq <= Fn . pq

fk . pq <= Fn . pq ; :: thesis: verum

end;assume A91: S

let k be Nat; :: thesis: ( k <> 0 & k <= i + 1 & i + 1 <= len SF implies for fk, Fn being RealMap of [:T,T:] st fk = SF . k & Fn = F . (i + 1) holds

fk . pq <= Fn . pq )

assume that

A92: k <> 0 and

A93: k <= i + 1 and

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

fk . pq <= Fn . pq

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

fk . pq <= Fn . pq

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

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: ( fk = SF . k & Fn = F . (i + 1) implies b_{1} . pq <= b_{2} . pq )

assume that

A95: fk = SF . k and

A96: Fn = F . (i + 1) ; :: thesis: b_{1} . pq <= b_{2} . pq

end;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: ( fk = SF . k & Fn = F . (i + 1) implies b

assume that

A95: fk = SF . k and

A96: Fn = F . (i + 1) ; :: thesis: b

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

end;

suppose A97:
k < i + 1
; :: thesis: b_{1} . pq <= b_{2} . pq

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

end;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: verum

suppose A102:
k = i + 1
; :: thesis: b_{1} . pq <= b_{2} . pq

end;

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

end;

suppose A103:
i <> 0
; :: thesis: b_{1} . pq <= b_{2} . pq

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

end;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: verum

fk . pq <= Fn . pq ; :: thesis: verum

A107: for i being Nat holds S

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

A113: now :: thesis: 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

1 = (min (jj,SumFTS9)) . [p,q]

A115:
for pq being Element of the carrier of [:T,T:]( 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

1 = (min (jj,SumFTS9)) . [p,q]

let p, q be Point of T; :: thesis: ( ex A, B being Subset of T st

( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies 1 = (min (jj,SumFTS9)) . [p,q] )

assume ex A, B being Subset of T st

( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; :: thesis: 1 = (min (jj,SumFTS9)) . [p,q]

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

end;( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) implies 1 = (min (jj,SumFTS9)) . [p,q] )

assume ex A, B being Subset of T st

( A is open & B is open & A in Bn . m & B in Bn . n & p in A & Cl A c= B & not q in B ) ; :: thesis: 1 = (min (jj,SumFTS9)) . [p,q]

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

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

map9 . pq = 0

proof

A116:
for pq1, pq2 being Point of [:T,T:] holds
let pq be Element of the carrier of [:T,T:]; :: thesis: for map9 being Element of Funcs ( the carrier of [:T,T:],REAL) st map9 is_a_unity_wrt ADD holds

map9 . pq = 0

let map9 be Element of Funcs ( the carrier of [:T,T:],REAL); :: thesis: ( map9 is_a_unity_wrt ADD implies map9 . pq = 0 )

assume map9 is_a_unity_wrt ADD ; :: thesis: map9 . pq = 0

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

end;map9 . pq = 0

let map9 be Element of Funcs ( the carrier of [:T,T:],REAL); :: thesis: ( map9 is_a_unity_wrt ADD implies map9 . pq = 0 )

assume map9 is_a_unity_wrt ADD ; :: thesis: map9 . pq = 0

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

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

SumFdist1 . pq1 >= SumFdist2 . pq1 ) )

proof

deffunc H_{5}( 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: ( ( 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 ) )

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_{4}(H_{3}(p1) \/ H_{3}(q1))
by A61;

A119: for p, q, p1, q1 being Point of T st [p,q] in SS . [p1,q1] holds

H_{5}(p,q) c= H_{3}(p1) \/ H_{3}(q1)
_{4}(H_{5}(p1,q1)) c= H_{4}(H_{3}(p1) \/ H_{3}(q1))

for p, q, p1, q1 being Point of T st rng f = H_{4}(H_{3}(p1) \/ H_{3}(q1)) \ H_{4}(H_{5}(p,q)) holds

(ADD "**" f) . [p,q] = 0_{4}(H_{3}(p1) \/ H_{3}(q1)) is finite
by A50;

then consider No being FinSequence such that

A157: rng No = H_{4}(H_{5}(p1,q1))
and

A158: No is one-to-one by A126, FINSEQ_4:58;

H_{4}(H_{3}(p1) \/ H_{3}(q1)) c= Funcs ( the carrier of [:T,T:],REAL)
by A50;

then A159: H_{4}(H_{5}(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_{4}(H_{3}(p2) \/ H_{3}(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_{4}(H_{5}(p1,q1)) /\ H_{4}(H_{3}(p2) \/ H_{3}(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_{4}(H_{5}(p1,q1)) /\ H_{4}(H_{3}(p2) \/ H_{3}(q2))
and

A167: NoiS2 is one-to-one by A126, A156, FINSEQ_4:58;

H_{4}(H_{5}(p1,q1)) /\ H_{4}(H_{3}(p2) \/ H_{3}(q2)) c= H_{4}(H_{5}(p1,q1))
by XBOOLE_1:17;

then H_{4}(H_{5}(p1,q1)) /\ H_{4}(H_{3}(p2) \/ H_{3}(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_{4}(H_{3}(p2) \/ H_{3}(q2)) \ H_{4}(H_{5}(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: for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds

SumFdist1 . pq1 >= SumFdist2 . pq1

SumFdist1 . pq1 >= SumFdist2 . pq1 ; :: thesis: verum

end;( not Fn . A = FnA or FnA . $1 > 0 or FnA . $2 > 0 ) ) ) } ;

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

SumFdist1 . pq1 >= SumFdist2 . pq1 ) )

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

A119: for p, q, p1, q1 being Point of T st [p,q] in SS . [p1,q1] holds

H

proof

A126:
H
let p, q, p1, q1 be Point of T; :: thesis: ( [p,q] in SS . [p1,q1] implies H_{5}(p,q) c= H_{3}(p1) \/ H_{3}(q1) )

assume A120: [p,q] in SS . [p1,q1] ; :: thesis: H_{5}(p,q) c= H_{3}(p1) \/ H_{3}(q1)

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: ( not no0 in H_{5}(p,q) or no0 in H_{3}(p1) \/ H_{3}(q1) )

assume no0 in H_{5}(p,q)
; :: thesis: no0 in H_{3}(p1) \/ H_{3}(q1)

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_{6}[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_{2}(Sx . p1) or A in H_{2}(Sx . q1) )
by A123;

then ( FnA in H_{3}(p1) or FnA in H_{3}(q1) )
by A123;

hence no0 in H_{3}(p1) \/ H_{3}(q1)
by A122, XBOOLE_0:def 3; :: thesis: verum

end;assume A120: [p,q] in SS . [p1,q1] ; :: thesis: H

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: ( not no0 in H

assume no0 in H

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

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

then ( FnA in H

hence no0 in H

proof

A128:
for f being FinSequence of Funcs ( the carrier of [:T,T:],REAL)
( 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_{5}(p1,q1) c= H_{3}(p1) \/ H_{3}(q1)
by A119;

let FD be object ; :: according to TARSKI:def 3 :: thesis: ( not FD in H_{4}(H_{5}(p1,q1)) or FD in H_{4}(H_{3}(p1) \/ H_{3}(q1)) )

assume FD in H_{4}(H_{5}(p1,q1))
; :: thesis: FD in H_{4}(H_{3}(p1) \/ H_{3}(q1))

then ex fd being RealMap of T st

( FD = Fdist . fd & fd in H_{5}(p1,q1) )
;

hence FD in H_{4}(H_{3}(p1) \/ H_{3}(q1))
by A127; :: thesis: verum

end;then [p1,q1] in [:(Sx . p1),(Sx . q1):] by ZFMISC_1:87;

then [p1,q1] in SS . [p1,q1] by A34;

then A127: H

let FD be object ; :: according to TARSKI:def 3 :: thesis: ( not FD in H

assume FD in H

then ex fd being RealMap of T st

( FD = Fdist . fd & fd in H

hence FD in H

for p, q, p1, q1 being Point of T st rng f = H

(ADD "**" f) . [p,q] = 0

proof

A156:
H
let f be FinSequence of Funcs ( the carrier of [:T,T:],REAL); :: thesis: for p, q, p1, q1 being Point of T st rng f = H_{4}(H_{3}(p1) \/ H_{3}(q1)) \ H_{4}(H_{5}(p,q)) holds

(ADD "**" f) . [p,q] = 0

let p, q, p1, q1 be Point of T; :: thesis: ( rng f = H_{4}(H_{3}(p1) \/ H_{3}(q1)) \ H_{4}(H_{5}(p,q)) implies (ADD "**" f) . [p,q] = 0 )

assume A129: rng f = H_{4}(H_{3}(p1) \/ H_{3}(q1)) \ H_{4}(H_{5}(p,q))
; :: thesis: (ADD "**" f) . [p,q] = 0

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

end;(ADD "**" f) . [p,q] = 0

let p, q, p1, q1 be Point of T; :: thesis: ( rng f = H

assume A129: rng f = H

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

now :: thesis: (ADD "**" f) . pq = 0 end;

hence
(ADD "**" f) . [p,q] = 0
; :: thesis: verumper cases
( len f = 0 or len f <> 0 )
;

end;

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

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

end;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: verum

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

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_{10}[ Nat] means ( $1 <> 0 & $1 <= len f implies (F . $1) . pq = 0 );

A137: for k being Nat st S_{10}[k] holds

S_{10}[k + 1]
_{10}[ 0 ]
;

for n being Nat holds S_{10}[n]
from NAT_1:sch 2(A155, A137);

hence (ADD "**" f) . pq = 0 by A133, A136; :: thesis: verum

end;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

A137: for k being Nat st S

S

proof

A155:
S
let k be Nat; :: thesis: ( S_{10}[k] implies S_{10}[k + 1] )

assume A138: S_{10}[k]
; :: thesis: S_{10}[k + 1]

assume that

k + 1 <> 0 and

A139: k + 1 <= len f ; :: thesis: (F . (k + 1)) . pq = 0

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_{4}(H_{3}(p1) \/ H_{3}(q1)) \ H_{4}(H_{5}(p,q))
by A129, FUNCT_1:def 3;

then f . (k + 1) in H_{4}(H_{3}(p1) \/ H_{3}(q1))
;

then consider fd being RealMap of T such that

A142: Fdist . fd = f . (k + 1) and

A143: fd in H_{3}(p1) \/ H_{3}(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_{4}(H_{5}(p,q))
by A141, XBOOLE_0:def 5;

A146: ( fd . p = 0 & fd . q = 0 )

end;assume A138: S

assume that

k + 1 <> 0 and

A139: k + 1 <= len f ; :: thesis: (F . (k + 1)) . pq = 0

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

then f . (k + 1) in H

then consider fd being RealMap of T such that

A142: Fdist . fd = f . (k + 1) and

A143: fd in H

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

A146: ( fd . p = 0 & fd . q = 0 )

proof

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

end;per cases
( fd in H_{3}(p1) or fd in H_{3}(q1) )
by A143, XBOOLE_0:def 3;

end;

suppose
fd in H_{3}(p1)
; :: thesis: contradiction

then consider A being Subset of T such that

A148: fd = Fn . A and

A149: A in Bn . n and

A in H_{2}(Sx . p1)
;

A150: S_{6}[A,Fn . A]
by A26, A149;

not fd in H_{5}(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: verum

end;A148: fd = Fn . A and

A149: A in Bn . n and

A in H

A150: S

not fd in H

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

suppose
fd in H_{3}(q1)
; :: thesis: contradiction

then consider A being Subset of T such that

A151: fd = Fn . A and

A152: A in Bn . n and

A in H_{2}(Sx . q1)
;

A153: S_{6}[A,Fn . A]
by A26, A152;

not fd in H_{5}(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: verum

end;A151: fd = Fn . A and

A152: A in Bn . n and

A in H

A153: S

not fd in H

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

for n being Nat holds S

hence (ADD "**" f) . pq = 0 by A133, A136; :: thesis: verum

then consider No being FinSequence such that

A157: rng No = H

A158: No is one-to-one by A126, FINSEQ_4:58;

H

then A159: H

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

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

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

A167: NoiS2 is one-to-one by A126, A156, FINSEQ_4:58;

H

then H

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

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: for SumFdist1, SumFdist2 being RealMap of [:T,T:] st SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 holds

SumFdist1 . pq1 >= SumFdist2 . pq1

proof

A182:
ANoNoiS2 . (p1,q1) >= 0
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: (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1

_{4}(H_{5}(p1,q1)) c= H_{4}(H_{3}(p2) \/ H_{3}(q2))
;

then H_{4}(H_{5}(p1,q1)) /\ H_{4}(H_{3}(p2) \/ H_{3}(q2)) = H_{4}(H_{5}(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: verum

end;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: (SumFdist . pq1) . pq1 = (SumFdist . pq2) . pq1

now :: thesis: for FD being object st FD in H_{4}(H_{5}(p1,q1)) holds

FD in H_{4}(H_{3}(p2) \/ H_{3}(q2))

then
HFD in H

let FD be object ; :: thesis: ( FD in H_{4}(H_{5}(p1,q1)) implies FD in H_{4}(H_{3}(p2) \/ H_{3}(q2)) )

assume FD in H_{4}(H_{5}(p1,q1))
; :: thesis: FD in H_{4}(H_{3}(p2) \/ H_{3}(q2))

then A180: ex fd being RealMap of T st

( FD = Fdist . fd & fd in H_{5}(p1,q1) )
;

H_{5}(p1,q1) c= H_{3}(p2) \/ H_{3}(q2)
by A119, A117, A160, A179;

hence FD in H_{4}(H_{3}(p2) \/ H_{3}(q2))
by A180; :: thesis: verum

end;assume FD in H

then A180: ex fd being RealMap of T st

( FD = Fdist . fd & fd in H

H

hence FD in H

then H

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

proof

set N = NoNoiS2;

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

end;

suppose A183:
len NoNoiS2 = 0
; :: thesis: ANoNoiS2 . (p1,q1) >= 0

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

end;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: verum

suppose A186:
len NoNoiS2 <> 0
; :: thesis: ANoNoiS2 . (p1,q1) >= 0

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_{10}[ 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_{10}[k] holds

S_{10}[k + 1]
_{10}[ 0 ]
;

for n being Nat holds S_{10}[n]
from NAT_1:sch 2(A201, A190);

hence ANoNoiS2 . (p1,q1) >= 0 by A186, A189; :: thesis: verum

end;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

Fn . (p1,q1) >= 0 );

A190: for k being Nat st S

S

proof

A201:
S
let k be Nat; :: thesis: ( S_{10}[k] implies S_{10}[k + 1] )

assume A191: S_{10}[k]
; :: thesis: S_{10}[k + 1]

assume that

k + 1 <> 0 and

A192: k + 1 <= len NoNoiS2 ; :: thesis: for Fn being RealMap of [:T,T:] st Fn = F . (k + 1) holds

Fn . (p1,q1) >= 0

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_{4}(H_{5}(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_{5}(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;

assume Fn = F . (k + 1) ; :: thesis: Fn . (p1,q1) >= 0

hence Fn . (p1,q1) >= 0 by A198; :: thesis: verum

end;assume A191: S

assume that

k + 1 <> 0 and

A192: k + 1 <= len NoNoiS2 ; :: thesis: for Fn being RealMap of [:T,T:] st Fn = F . (k + 1) holds

Fn . (p1,q1) >= 0

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

then consider fd being RealMap of T such that

A194: Fdist . fd = NoNoiS2 . (k + 1) and

fd in H

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: Fk1 . (p1,q1) >= 0 end;

let Fn be RealMap of [:T,T:]; :: thesis: ( Fn = F . (k + 1) implies Fn . (p1,q1) >= 0 )per cases
( k = 0 or k > 0 )
;

end;

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

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

end;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: verum

assume Fn = F . (k + 1) ; :: thesis: Fn . (p1,q1) >= 0

hence Fn . (p1,q1) >= 0 by A198; :: thesis: verum

for n being Nat holds S

hence ANoNoiS2 . (p1,q1) >= 0 by A186, A189; :: thesis: verum

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

SumFdist1 . pq1 >= SumFdist2 . pq1

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

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: ( SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 implies SumFdist1 . pq1 >= SumFdist2 . pq1 )

assume that

A203: SumFdist1 = SumFdist . pq1 and

A204: SumFdist2 = SumFdist . pq2 ; :: thesis: SumFdist1 . pq1 >= SumFdist2 . pq1

SumFdist2 = AS2 by A63, A204;

hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A63, A117, A203, A202; :: thesis: verum

end;let SumFdist1, SumFdist2 be RealMap of [:T,T:]; :: thesis: ( SumFdist1 = SumFdist . pq1 & SumFdist2 = SumFdist . pq2 implies SumFdist1 . pq1 >= SumFdist2 . pq1 )

assume that

A203: SumFdist1 = SumFdist . pq1 and

A204: SumFdist2 = SumFdist . pq2 ; :: thesis: SumFdist1 . pq1 >= SumFdist2 . pq1

SumFdist2 = AS2 by A63, A204;

hence SumFdist1 . pq1 >= SumFdist2 . pq1 by A63, A117, A203, A202; :: thesis: verum

SumFdist1 . pq1 >= SumFdist2 . pq1 ; :: thesis: verum

now :: thesis: for p, q, r being Point of T holds

( SumFTS . (p,p) = 0 & SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) )

then A249:
SumFTS is_a_pseudometric_of the carrier of T
by NAGATA_1:28;( SumFTS . (p,p) = 0 & SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q)) )

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

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

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

proof

thus
SumFTS . (p,r) <= (SumFTS . (p,q)) + (SumFTS . (r,q))
:: thesis: verum
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;

hence SumFTS . (p,p) = 0 by A205, NAGATA_1:def 8; :: thesis: verum

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

A205: now :: thesis: (ADD "**" SF) . pp = 0 end;

SumFdist . pp = ADD "**" SF
by A63;per cases
( len SF = 0 or len SF <> 0 )
;

end;

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

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

end;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: verum

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

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_{10}[ Nat] means ( $1 <> 0 & $1 <= len SF implies (F . $1) . pp = 0 );

A213: for k being Nat st S_{10}[k] holds

S_{10}[k + 1]
_{10}[ 0 ]
;

for n being Nat holds S_{10}[n]
from NAT_1:sch 2(A221, A213);

hence (ADD "**" SF) . pp = 0 by A209, A212; :: thesis: verum

end;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

A213: for k being Nat st S

S

proof

A221:
S
let k be Nat; :: thesis: ( S_{10}[k] implies S_{10}[k + 1] )

assume A214: S_{10}[k]
; :: thesis: S_{10}[k + 1]

consider x, y being Point of T such that

[x,y] = pp and

A215: rng SF = H_{4}(H_{3}(x) \/ H_{3}(y))
by A61;

assume that

k + 1 <> 0 and

A216: k + 1 <= len SF ; :: thesis: (F . (k + 1)) . pp = 0

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_{4}(H_{3}(x) \/ H_{3}(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_{3}(x) \/ H_{3}(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;

end;assume A214: S

consider x, y being Point of T such that

[x,y] = pp and

A215: rng SF = H

assume that

k + 1 <> 0 and

A216: k + 1 <= len SF ; :: thesis: (F . (k + 1)) . pp = 0

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

then consider fd being RealMap of T such that

A218: Fdist . fd = SF . (k + 1) and

fd in H

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;

for n being Nat holds S

hence (ADD "**" SF) . pp = 0 by A209, A212; :: thesis: verum

hence SumFTS . (p,p) = 0 by A205, NAGATA_1:def 8; :: thesis: verum

proof

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;

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

end;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: ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq)end;

SumFpr = ADD "**" SFpr
by A63;per cases
( len SFpr = 0 or len SFpr <> 0 )
;

end;

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

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

end;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: verum

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

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_{10}[ 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_{10}[k] holds

S_{10}[k + 1]
_{10}[ 0 ]
;

for n being Nat holds S_{10}[n]
from NAT_1:sch 2(A248, A233);

hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A229, A232; :: thesis: verum

end;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

F9 . pr <= (F9 . pq) + (F9 . rq) );

A233: for k being Nat st S

S

proof

A248:
S
let k be Nat; :: thesis: ( S_{10}[k] implies S_{10}[k + 1] )

assume A234: S_{10}[k]
; :: thesis: S_{10}[k + 1]

consider x, y being Point of T such that

[x,y] = pr and

A235: rng SFpr = H_{4}(H_{3}(x) \/ H_{3}(y))
by A61;

assume that

k + 1 <> 0 and

A236: k + 1 <= len SFpr ; :: thesis: for F9 being RealMap of [:T,T:] st F9 = F . (k + 1) holds

F9 . pr <= (F9 . pq) + (F9 . rq)

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_{4}(H_{3}(x) \/ H_{3}(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_{3}(x) \/ H_{3}(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: ( F9 = F . (k + 1) implies F9 . pr <= (F9 . pq) + (F9 . rq) )

assume A244: F9 = F . (k + 1) ; :: thesis: F9 . pr <= (F9 . pq) + (F9 . rq)

end;assume A234: S

consider x, y being Point of T such that

[x,y] = pr and

A235: rng SFpr = H

assume that

k + 1 <> 0 and

A236: k + 1 <= len SFpr ; :: thesis: for F9 being RealMap of [:T,T:] st F9 = F . (k + 1) holds

F9 . pr <= (F9 . pq) + (F9 . rq)

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

then consider fd being RealMap of T such that

A238: Fdist . fd = SFpr . (k + 1) and

fd in H

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: ( F9 = F . (k + 1) implies F9 . pr <= (F9 . pq) + (F9 . rq) )

assume A244: F9 = F . (k + 1) ; :: thesis: F9 . pr <= (F9 . pq) + (F9 . rq)

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

end;

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

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

end;suppose A245:
k > 0
; :: thesis: F9 . pr <= (F9 . pq) + (F9 . rq)

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

end;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: verum

for n being Nat holds S

hence ASFpr . pr <= (ASFpr . pq) + (ASFpr . rq) by A229, A232; :: thesis: verum

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

A250: for p being Point of T

for fd being Element of Funcs ( the carrier of T,REAL) st fd in H

( S

proof

A254:
for pq9 being Point of [:T,T:] holds SumFdist . pq9 is continuous RealMap of [:T,T:]
let p be Point of T; :: thesis: for fd being Element of Funcs ( the carrier of T,REAL) st fd in H_{3}(p) holds

( S_{4}[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )

let fd be Element of Funcs ( the carrier of T,REAL); :: thesis: ( fd in H_{3}(p) implies ( S_{4}[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] ) )

reconsider FD = Fdist . fd as RealMap of [:T,T:] by FUNCT_2:66;

assume fd in H_{3}(p)
; :: thesis: ( S_{4}[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )

then consider A being Subset of T such that

A251: fd = Fn . A and

A252: A in Bn . n and

A in H_{2}(Sx . p)
;

A253: S_{4}[fd,Fdist . fd]
by A46;

S_{6}[A,Fn . A]
by A26, A252;

then FD is continuous by A251, A253, NAGATA_1:21;

hence ( S_{4}[fd,Fdist . fd] & Fdist . fd is continuous RealMap of [:T,T:] )
by A46; :: thesis: verum

end;( S

let fd be Element of Funcs ( the carrier of T,REAL); :: thesis: ( fd in H

reconsider FD = Fdist . fd as RealMap of [:T,T:] by FUNCT_2:66;

assume fd in H

then consider A being Subset of T such that

A251: fd = Fn . A and

A252: A in Bn . n and

A in H

A253: S

S

then FD is continuous by A251, A253, NAGATA_1:21;

hence ( S

proof

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: SumFdist . pq9 is continuous RealMap of [:T,T:]

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_{4}(H_{3}(p) \/ H_{3}(q))
by A61;

for n being Element of NAT st 0 <> n & n <= len SF holds

SF . n is continuous RealMap of [:T,T:]

hence SumFdist . pq9 is continuous RealMap of [:T,T:] by A63; :: thesis: verum

end;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

for n being Element of NAT st 0 <> n & n <= len SF holds

SF . n is continuous RealMap of [:T,T:]

proof

then
ADD "**" SF is continuous RealMap of [:T,T:]
by A64, NAGATA_1:25;
let n be Element of NAT ; :: thesis: ( 0 <> n & n <= len SF implies SF . n is continuous RealMap of [:T,T:] )

assume that

A256: 0 <> n and

A257: n <= len SF ; :: thesis: SF . n is continuous RealMap of [:T,T:]

n >= 1 by A256, NAT_1:14;

then n in dom SF by A257, FINSEQ_3:25;

then SF . n in H_{4}(H_{3}(p) \/ H_{3}(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_{3}(p) \/ H_{3}(q)
;

A260: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;

( fd in H_{3}(p) or fd in H_{3}(q) )
by A259, XBOOLE_0:def 3;

hence SF . n is continuous RealMap of [:T,T:] by A250, A258, A260; :: thesis: verum

end;assume that

A256: 0 <> n and

A257: n <= len SF ; :: thesis: SF . n is continuous RealMap of [:T,T:]

n >= 1 by A256, NAT_1:14;

then n in dom SF by A257, FINSEQ_3:25;

then SF . n in H

then consider fd being RealMap of T such that

A258: SF . n = Fdist . fd and

A259: fd in H

A260: fd in Funcs ( the carrier of T,REAL) by FUNCT_2:8;

( fd in H

hence SF . n is continuous RealMap of [:T,T:] by A250, A258, A260; :: thesis: verum

hence SumFdist . pq9 is continuous RealMap of [:T,T:] by A63; :: thesis: verum

proof

take
min (jj,SumFTS9)
; :: thesis: S
let pq9 be Point of [:T,T:]; :: thesis: SumFdist9 . pq9 is continuous Function of [:T,T:],R^1

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

end;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: verum

A262: for p, q being Point of T holds (min (jj,SumFTS9)) . [p,q] <= 1

proof

for p, q being Point of [:T,T:] st p in SS . q holds
let p, q be Point of T; :: thesis: (min (jj,SumFTS9)) . [p,q] <= 1

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

end;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: verum

(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

ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S

proof

consider F being sequence of (Funcs ( the carrier of [:T,T:],REAL)) such that
A264:
NAT = rng PairFunc
by Th2, FUNCT_2:def 3;

let k be object ; :: thesis: ( k in NAT implies ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S_{2}[k,f] ) )

assume k in NAT ; :: thesis: ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S_{2}[k,f] )

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_{1}[n,m,pmet9]
by A7, A267;

take pmet9 ; :: thesis: ( pmet9 in Funcs ( the carrier of [:T,T:],REAL) & S_{2}[k,pmet9] )

thus pmet9 in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8; :: thesis: S_{2}[k,pmet9]

take pm = pmet9; :: thesis: ( pm = pmet9 & ( for n, m being Nat st (PairFunc ") . k = [n,m] holds

S_{1}[n,m,pm] ) )

thus pm = pmet9 ; :: thesis: for n, m being Nat st (PairFunc ") . k = [n,m] holds

S_{1}[n,m,pm]

let n1, m1 be Nat; :: thesis: ( (PairFunc ") . k = [n1,m1] implies S_{1}[n1,m1,pm] )

assume (PairFunc ") . k = [n1,m1] ; :: thesis: S_{1}[n1,m1,pm]

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_{1}[n1,m1,pm]
by A269; :: thesis: verum

end;let k be object ; :: thesis: ( k in NAT implies ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S

assume k in NAT ; :: thesis: ex f being object st

( f in Funcs ( the carrier of [:T,T:],REAL) & S

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

take pmet9 ; :: thesis: ( pmet9 in Funcs ( the carrier of [:T,T:],REAL) & S

thus pmet9 in Funcs ( the carrier of [:T,T:],REAL) by FUNCT_2:8; :: thesis: S

take pm = pmet9; :: thesis: ( pm = pmet9 & ( for n, m being Nat st (PairFunc ") . k = [n,m] holds

S

thus pm = pmet9 ; :: thesis: for n, m being Nat st (PairFunc ") . k = [n,m] holds

S

let n1, m1 be Nat; :: thesis: ( (PairFunc ") . k = [n1,m1] implies S

assume (PairFunc ") . k = [n1,m1] ; :: thesis: S

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

A270: for n being object st n in NAT holds

S

A271: now :: thesis: for n being Nat holds F . n is PartFunc of [: the carrier of T, the carrier of T:],REAL

dom F = NAT
by FUNCT_2:def 1;let n be Nat; :: thesis: F . n is PartFunc of [: the carrier of T, the carrier of T:],REAL

[: 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: verum

end;[: 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: verum

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

proof

for k being Nat ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
let p be Point of T; :: thesis: 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 A9 be non empty Subset of T; :: thesis: ( not p in A9 & A9 is closed implies 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 )

assume that

A273: not p in A9 and

A274: A9 is closed ; :: thesis: 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

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_{1}[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

(lower_bound (pmet,A9)) . p > 0

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

end;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 A9 be non empty Subset of T; :: thesis: ( not p in A9 & A9 is closed implies 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 )

assume that

A273: not p in A9 and

A274: A9 is closed ; :: thesis: 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

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

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

proof

take
PairFunc . [n,m]
; :: thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st F9 . (PairFunc . [n,m]) = pmet holds
let rn be Real; :: thesis: ( rn in (dist (pmet,p)) .: A9 implies rn >= 1 )

assume rn in (dist (pmet,p)) .: A9 ; :: thesis: rn >= 1

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

end;assume rn in (dist (pmet,p)) .: A9 ; :: thesis: rn >= 1

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

(lower_bound (pmet,A9)) . p > 0

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

( 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 ) )

proof

hence
T is metrizable
by A2, A272, Th17; :: thesis: verum
let k be Nat; :: thesis: 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 ) )

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_{1}[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: ( 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 ) )

thus ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A295, A301, A303; :: thesis: ( ( 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 ) )

thus for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 :: thesis: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous

pmet9 is continuous by A301, A302; :: thesis: verum

end;( 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 ) )

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

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

thus ( F9 . k = pmet & pmet is_a_pseudometric_of the carrier of T ) by A295, A301, A303; :: thesis: ( ( 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 ) )

thus for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= 1 :: thesis: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds

pmet9 is continuous

proof

thus
for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
let pq be Element of [: the carrier of T, the carrier of T:]; :: thesis: pmet . pq <= 1

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

end;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: verum

pmet9 is continuous by A301, A302; :: thesis: verum