:: The {N}agata-Smirnov Theorem. {P}art {II} :: by Karol P\c{a}k :: :: Received July 22, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, XREAL_0, ORDINAL1, XBOOLE_0, PRE_TOPC, ZFMISC_1, STRUCT_0, FUNCT_1, PSCOMP_1, SEQFUNC, SEQ_1, XXREAL_0, CARD_1, NEWTON, RELAT_1, ARYTM_3, INT_1, NAT_1, ARYTM_1, FUNCT_7, FUNCT_2, TARSKI, METRIC_1, RCOMP_1, MCART_1, SETFAM_1, ORDINAL2, TOPMETR, TMAP_1, SEQ_4, NAGATA_1, XXREAL_2, COMPLEX1, RELAT_2, VALUED_0, PCOMPS_1, PBOOLE, SERIES_1, CARD_3, VALUED_1, SEQ_2, FINSEQ_1, PREPOWER, BINOP_1, SETWISEO, FINSOP_1, ORDINAL4, CARD_5, RLVECT_3, FINSET_1, COH_SP, PARTFUN1, WELLORD1, PCOMPS_2, NATTRA_1, NAGATA_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, SETWISEO, BORSUK_1, RELAT_1, RELAT_2, ORDINAL1, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, FUNCT_1, COMPLEX1, REAL_1, RELSET_1, PARTFUN1, VALUED_0, VALUED_1, SEQ_1, FUNCT_2, FUNCT_3, DOMAIN_1, BINOP_1, PRE_TOPC, NAT_1, NAT_D, CARD_1, NUMBERS, FINSET_1, STRUCT_0, FINSEQ_1, PCOMPS_1, PCOMPS_2, NEWTON, TOPS_2, METRIC_1, PROB_1, SEQFUNC, PREPOWER, TOPMETR, PSCOMP_1, TMAP_1, NAGATA_1, SEQ_2, SEQ_4, SERIES_1, FINSOP_1, CANTOR_1, WELLORD1, FUNCT_7; constructors WELLORD1, FUNCT_3, SETWISEO, REAL_1, NAT_D, PROB_1, FINSOP_1, NEWTON, PREPOWER, SERIES_1, FUNCT_7, TOPS_2, TMAP_1, CANTOR_1, PCOMPS_2, NAGATA_1, SEQ_1, BORSUK_4, SEQFUNC, SEQ_4, BINOP_2, SEQ_2, PSCOMP_1, PCOMPS_1, COMSEQ_2; registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, TOPS_1, METRIC_1, BORSUK_1, TOPMETR, TOPREAL6, VALUED_0, VALUED_1, FUNCT_2, CARD_1, PRE_TOPC, FUNCT_1, PSCOMP_1; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; definitions FUNCT_2, TARSKI, TOPS_2, XBOOLE_0, BINOP_1, SUBSET_1, STRUCT_0, XXREAL_2; theorems NAT_1, NEWTON, FUNCT_2, PCOMPS_1, PCOMPS_2, NAGATA_1, SUBSET_1, METRIC_6, FUNCT_3, FUNCT_1, METRIC_1, XCMPLX_1, ABSVALUE, TOPMETR, TMAP_1, BORSUK_1, XBOOLE_1, TARSKI, SETFAM_1, XBOOLE_0, TOPS_1, TOPS_2, PRE_TOPC, FINSEQ_1, CARD_4, ZFMISC_1, BINOP_1, SEQ_2, SEQ_4, SEQ_1, SERIES_1, PREPOWER, SEQFUNC, PARTFUN1, JGRAPH_2, URYSOHN1, FINSEQ_3, FINSEQ_4, FINSOP_1, SETWISEO, PROB_1, URYSOHN3, WELLORD1, WELLORD2, TBSP_1, RELAT_1, RELAT_2, YELLOW_9, FUNCT_7, RSSPACE2, RSSPACE, BHSP_5, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, VALUED_1, XXREAL_2, JORDAN5A, XTUPLE_0; schemes FUNCT_2, NAT_1, SEQFUNC, FRAENKEL, BINOP_1, PCOMPS_2; begin reserve i, k, m, n for Element of NAT, r, s for Real, rn for real number, x, y , z, X for set, T, T1, T2 for non empty TopSpace, p, q for Point of T, A, B, C for Subset of T, A9 for non empty Subset of T, pq for Element of [:the carrier of T,the carrier of T:], pq9 for Point of [:T,T:], pmet,pmet1 for Function of [:the carrier of T,the carrier of T:],REAL, pmet9,pmet19 for RealMap of [:T,T:] , f,f1 for RealMap of T, FS2 for Functional_Sequence of [:the carrier of T,the carrier of T:],REAL, seq for Real_Sequence; theorem Th1: for i st i>0 ex n,m st i=(2|^n)*(2*m+1) proof defpred N[Element of NAT] means for k st 1<=k & k<=$1 ex n,m st k=(2|^n)*(2* m+1); A1: for i st N[i] holds N[i + 1] proof let i such that A2: N[i]; let k such that A3: 1<=k and A4: k <=i+1; now per cases by A4,XXREAL_0:1; suppose A5: k=i+1 & i=0; set m=0; A6: 1=2|^0 by NEWTON:4; k=1*(m*2+1) by A5; hence thesis by A6; end; suppose A7: k=i+1 & i>0; per cases by NAT_D:12; suppose k mod 2=1; then consider m being Nat such that A8: k = 2 * m + 1 and 1<2 by NAT_D:def 2; reconsider m as Element of NAT by ORDINAL1:def 12; 1=2|^0 by NEWTON:4; then k=(2|^0)*(2*m+1) by A8; hence thesis; end; suppose k mod 2=0; then consider j being Nat such that A9: k = 2 * j + 0 and 0<2 by NAT_D:def 2; reconsider j as Element of NAT by ORDINAL1:def 12; A10: j<=i proof assume j>i; then j+j>i+1 by NAT_1:14,XREAL_1:8; hence thesis by A7,A9; end; j<>0 by A7,A9; then j>=1 by NAT_1:14; then consider n,m such that A11: j=(2|^n)*(2*m+1) by A2,A10; k=(2*(2|^n))*(2*m+1) by A9,A11; then k=(2|^(n+1))*(2*m+1) by NEWTON:6; hence thesis; end; end; suppose k0; then A12: i>=1 by NAT_1:14; A13: N[ 0 ]; for n holds N[n] from NAT_1:sch 1(A13,A1); hence thesis by A12; end; definition func PairFunc -> Function of [:NAT,NAT:],NAT means :Def1: for n,m holds it.[ n,m] = (2|^n)*(2*m+1)-1; existence proof deffunc N(Element of NAT,Element of NAT) = In((2|^$1)*(2*$2+1)-1,NAT); A1: for n,m be Element of NAT holds (2|^n)*(2*m+1)-1 in NAT proof let n,m be Element of NAT; 0 < 2|^n by NEWTON:83; then ((2|^n)*(2*m+1))-1 is Element of NAT by NAT_1:20,XREAL_1:129; hence thesis; end; consider NN being Function of [:NAT,NAT:],NAT such that A2: for n,m being Element of NAT holds NN.(n,m) = N(n,m) from BINOP_1: sch 4; take NN; let n,m; NN.(n,m) = In((2|^n)*(2*m+1)-1,NAT) by A2 .= (2|^n)*(2*m+1)-1 by A1,FUNCT_7:def 1; hence thesis; end; uniqueness proof let N1,N2 be Function of [:NAT,NAT:],NAT; assume that A3: for n,m holds N1.[n,m] = (2|^n)*(2*m+1)-1 and A4: for n,m holds N2.[n,m] = (2|^n)*(2*m+1)-1; now let n,m be Element of NAT; N1.[n,m] = (2|^n)*(2*m+1)-1 by A3; hence N1.(n,m)=N2.(n,m) by A4; end; hence thesis by BINOP_1:2; end; end; theorem Th2: PairFunc is bijective proof now let nm1,nm2 be set; assume that A1: nm1 in [:NAT,NAT:] and A2: nm2 in [:NAT,NAT:] and A3: PairFunc.nm1=PairFunc.nm2; consider n2,m2 be set such that A4: n2 in NAT & m2 in NAT and A5: [n2,m2]=nm2 by A2,ZFMISC_1:def 2; consider n1,m1 be set such that A6: n1 in NAT & m1 in NAT and A7: [n1,m1]=nm1 by A1,ZFMISC_1:def 2; reconsider n1,n2,m1,m2 as Element of NAT by A6,A4; A8: (2|^n2)*(2*m2+1)-1=PairFunc.nm2 by A5,Def1; A9: (2|^n1)*(2*m1+1)-1=PairFunc.nm1 by A7,Def1; then n1=n2 by A3,A8,CARD_4:4; hence nm1=nm2 by A3,A7,A5,A9,A8,CARD_4:4; end; hence PairFunc is one-to-one by FUNCT_2:19; now let i be set; assume i in NAT; then reconsider i9=i as Element of NAT; consider n, m be Element of NAT such that A10: i9+1=(2|^n) *(2*m+1) by Th1; i9-0=((2|^n) *(2*m+1))-1 by A10; then dom PairFunc = [:NAT,NAT:] & i= PairFunc.[n,m] by Def1,FUNCT_2:def 1; hence i in rng PairFunc by FUNCT_1:def 3; end; then NAT c= rng PairFunc by TARSKI:def 3; then NAT=rng PairFunc by XBOOLE_0:def 10; hence PairFunc is onto by FUNCT_2:def 3; end; definition let X be set,f be Function of [:X,X:],REAL,x be Element of X; func dist(f,x) -> Function of X,REAL means :Def2: for y be Element of X holds it.y = f.(x,y); existence proof deffunc D(set)=f.(x,$1); A1: for y being set st y in X holds D(y) in REAL proof let y be set; assume y in X; f.[x,y] in REAL; hence thesis; end; consider DIST be Function of X,REAL such that A2: for y being set st y in X holds DIST.y =D(y) from FUNCT_2:sch 2(A1 ); now per cases; suppose A3: X is empty; let y be Element of X; not [x,y] in dom f by A3; then A4: f.[x,y]={} by FUNCT_1:def 2; not y in dom DIST by A3; hence f.(x,y)=DIST.y by A4,FUNCT_1:def 2; end; suppose X is non empty; hence for y be Element of X holds DIST.y = f.(x,y) by A2; end; end; hence thesis; end; uniqueness proof let D1,D2 be Function of X,REAL; assume that A5: for y be Element of X holds D1.y=f.(x,y) and A6: for y be Element of X holds D2.y=f.(x,y); now let y be Element of X; D1.y=f.(x,y) by A5; hence D1.y=D2.y by A6; end; hence thesis by FUNCT_2:63; end; end; theorem Th3: for D be Subset of [:T1,T2:] st D is open for x1 be Point of T1, x2 be Point of T2 for X1 be Subset of T1,X2 be Subset of T2 holds (X1=pr1(the carrier of T1,the carrier of T2).:(D/\[:the carrier of T1,{x2}:]) implies X1 is open) & (X2=pr2(the carrier of T1,the carrier of T2).:(D/\[:{x1},the carrier of T2:]) implies X2 is open) proof set cT1 =the carrier of T1; set cT2=the carrier of T2; let D be Subset of [:T1,T2:]; assume D is open; then consider FA be Subset-Family of [:T1,T2:] such that A1: D=union FA and A2: for B be set st B in FA ex B1 being Subset of T1, B2 being Subset of T2 st B = [:B1,B2:] & B1 is open & B2 is open by BORSUK_1:5; let x1 be Point of T1, x2 be Point of T2; let X1 be Subset of T1,X2 be Subset of T2; thus X1=pr1(cT1,cT2).:(D/\[:cT1,{x2}:]) implies X1 is open proof assume A3: X1=pr1(cT1,cT2).:(D/\[:cT1,{x2}:]); for t be set holds t in X1 iff ex U be Subset of T1 st U is open & U c= X1 & t in U proof let t be set; t in X1 implies ex U be Subset of T1 st U is open & U c= X1 & t in U proof assume t in X1; then consider tx be set such that A4: tx in dom pr1(cT1,cT2) and A5: tx in (D/\[:cT1,{x2}:]) and A6: t=pr1(cT1,cT2).tx by A3,FUNCT_1:def 6; tx in D by A5,XBOOLE_0:def 4; then consider tX be set such that A7: tx in tX and A8: tX in FA by A1,TARSKI:def 4; consider tX1 be Subset of T1,tX2 be Subset of T2 such that A9: tX=[:tX1,tX2:] and A10: tX1 is open and tX2 is open by A2,A8; take tX1; thus tX1 is open by A10; consider tx1,tx2 be set such that A11: tx1 in cT1 & tx2 in cT2 and A12: tx=[tx1,tx2] by A4,ZFMISC_1:def 2; thus tX1 c=X1 proof tx in [:cT1,{x2}:] by A5,XBOOLE_0:def 4; then A13: tx2=x2 by A12,ZFMISC_1:106; let a be set such that A14: a in tX1; [a,x2] in [:cT1,cT2:] by A14,ZFMISC_1:87; then A15: [a,x2] in dom pr1(cT1,cT2) by FUNCT_3:def 4; tx2 in tX2 by A12,A7,A9,ZFMISC_1:87; then [a,x2] in [:tX1,tX2:] by A14,A13,ZFMISC_1:87; then A16: [a,x2] in union FA by A8,A9,TARSKI:def 4; [a,x2] in [:cT1,{x2}:] by A14,ZFMISC_1:106; then [a,x2] in D/\[:cT1,{x2}:] by A1,A16,XBOOLE_0:def 4; then pr1(cT1,cT2).(a,x2) in pr1(cT1,cT2).:(D/\[:cT1,{x2}:]) by A15, FUNCT_1:def 6; hence thesis by A3,A14,FUNCT_3:def 4; end; pr1(cT1,cT2).(tx1,tx2)=tx1 by A11,FUNCT_3:def 4; hence thesis by A6,A12,A7,A9,ZFMISC_1:87; end; hence thesis; end; hence thesis by TOPS_1:25; end; thus X2= pr2(cT1,cT2).:(D/\[:{x1},cT2:]) implies X2 is open proof assume A17: X2=pr2(cT1,cT2).:(D/\[:{x1},cT2:]); for t be set holds t in X2 iff ex U be Subset of T2 st U is open & U c= X2 & t in U proof let t be set; t in X2 implies ex U be Subset of T2 st U is open & U c= X2 & t in U proof assume t in X2; then consider tx be set such that A18: tx in dom pr2(cT1,cT2) and A19: tx in (D/\[:{x1},cT2:]) and A20: t=pr2(cT1,cT2).tx by A17,FUNCT_1:def 6; tx in D by A19,XBOOLE_0:def 4; then consider tX be set such that A21: tx in tX and A22: tX in FA by A1,TARSKI:def 4; consider tx1,tx2 be set such that A23: tx1 in cT1 & tx2 in cT2 and A24: tx=[tx1,tx2] by A18,ZFMISC_1:def 2; A25: pr2(cT1,cT2).(tx1,tx2)=tx2 by A23,FUNCT_3:def 5; consider tX1 be Subset of T1,tX2 be Subset of T2 such that A26: tX=[:tX1,tX2:] and tX1 is open and A27: tX2 is open by A2,A22; A28: tX2 c=X2 proof tx in [:{x1},cT2:] by A19,XBOOLE_0:def 4; then A29: tx1=x1 by A24,ZFMISC_1:105; let a be set such that A30: a in tX2; [x1,a] in [:cT1,cT2:] by A30,ZFMISC_1:87; then A31: [x1,a] in dom pr2(cT1,cT2) by FUNCT_3:def 5; tx1 in tX1 by A24,A21,A26,ZFMISC_1:87; then [x1,a] in [:tX1,tX2:] by A30,A29,ZFMISC_1:87; then A32: [x1,a] in union FA by A22,A26,TARSKI:def 4; [x1,a] in [:{x1},cT2:] by A30,ZFMISC_1:105; then [x1,a] in D/\[:{x1},cT2:] by A1,A32,XBOOLE_0:def 4; then pr2(cT1,cT2).(x1,a) in pr2(cT1,cT2).:(D/\[:{x1},cT2:]) by A31, FUNCT_1:def 6; hence thesis by A17,A30,FUNCT_3:def 5; end; tx2 in tX2 by A24,A21,A26,ZFMISC_1:87; hence thesis by A20,A24,A27,A25,A28; end; hence thesis; end; hence thesis by TOPS_1:25; end; end; theorem Th4: for pmet st for pmet9 st pmet=pmet9 holds pmet9 is continuous for x be Point of T holds dist(pmet,x) is continuous proof set cT=the carrier of T; let pmet such that A1: for pmet9 st pmet=pmet9 holds pmet9 is continuous; [:cT,cT:]= the carrier of [:T,T:] by BORSUK_1:def 2; then reconsider pmet9=pmet as RealMap of [:T,T:]; reconsider pmetR=pmet9 as Function of [:T,T:],R^1 by TOPMETR:17; let x be Point of T; reconsider distx=dist(pmet,x) as Function of T,R^1 by TOPMETR:17; pmet9 is continuous by A1; then A2: pmetR is continuous by JORDAN5A:27; now let t be Point of T; for R being Subset of R^1 st R is open & distx.t in R ex U being Subset of T st U is open & t in U & distx.:U c= R proof reconsider xt=[x,t] as Point of [:T,T:] by BORSUK_1:def 2; A3: dom pr2(cT,cT)=[:cT,cT:] by FUNCT_3:def 5; A4: pmetR is_continuous_at xt & distx.t=pmet.(x,t) by A2,Def2,TMAP_1:50; let R be Subset of R^1; assume R is open & distx.t in R; then consider XU be Subset of [:T,T:] such that A5: XU is open and A6: xt in XU and A7: pmetR.:XU c= R by A4,TMAP_1:43; set U=pr2(cT,cT).:(XU/\[:{x},cT:]); [x,t] in [:{x},cT:] by ZFMISC_1:105; then [x,t] in XU/\[:{x},cT:] by A6,XBOOLE_0:def 4; then pr2(cT,cT).(x,t) in pr2(cT,cT).:(XU/\[:{x},cT:]) by A3,FUNCT_1:def 6 ; then A8: t in U by FUNCT_3:def 5; A9: distx.:U c= R proof let du be set; assume du in distx.:U; then consider u be set such that A10: u in dom distx and A11: u in U and A12: distx.u=du by FUNCT_1:def 6; reconsider u as Point of T by A10; consider xu be set such that A13: xu in dom pr2(cT,cT) and A14: xu in (XU/\[:{x},cT:]) and A15: pr2(cT,cT).xu=u by A11,FUNCT_1:def 6; consider x9,u9 be set such that A16: x9 in cT & u9 in cT and A17: xu=[x9,u9] by A13,ZFMISC_1:def 2; reconsider x9,u9 as Point of T by A16; [x9,u9] in [:{x},cT:] by A14,A17,XBOOLE_0:def 4; then pr2(cT,cT).(x9,u9) = u9 & x9=x by FUNCT_3:def 5,ZFMISC_1:105; then A18: pmet.(x9,u9)=du by A12,A15,A17,Def2; A19: dom pmetR=the carrier of [:T,T:] by FUNCT_2:def 1; [x9,u9] in XU by A14,A17,XBOOLE_0:def 4; then du in pmetR.:XU by A18,A19,FUNCT_1:def 6; hence thesis by A7; end; U is open by A5,Th3; hence thesis by A8,A9; end; hence distx is_continuous_at t by TMAP_1:43; end; then distx is continuous by TMAP_1:50; hence thesis by JORDAN5A:27; end; definition let X be non empty set,f be Function of [:X,X:],REAL,A be Subset of X; func lower_bound(f,A) -> Function of X,REAL means :Def3: for x be Element of X holds it.x = lower_bound((dist(f,x)).:A); existence proof deffunc I(Element of X)=lower_bound((dist(f,$1)).:A); consider INF be Function of X,REAL such that A1: for x being Element of X holds INF.x = I(x) from FUNCT_2:sch 4; take INF; thus thesis by A1; end; uniqueness proof let I1,I2 be Function of X,REAL; assume that A2: for x be Element of X holds I1.x=lower_bound((dist(f,x)).:A) and A3: for x be Element of X holds I2.x=lower_bound((dist(f,x)).:A); now let x be Element of X; I1.x=lower_bound((dist(f,x)).:A) by A2; hence I1.x=I2.x by A3; end; hence thesis by FUNCT_2:63; end; end; Lm1: for X be non empty set,f be Function of [:X,X:],REAL st f is_a_pseudometric_of X holds f is bounded_below & for A be non empty Subset of X,x be Element of X holds dist(f,x).:A is non empty bounded_below proof let X be non empty set,f be Function of [:X,X:],REAL such that A1: f is_a_pseudometric_of X; A2: now let A be non empty Subset of X,x be Element of X; A3: 0 is LowerBound of dist(f,x).:A proof let rn be ext-real number; assume rn in dist(f,x).:A; then consider y such that A4: y in dom dist(f,x) and y in A and A5: rn = dist(f,x).y by FUNCT_1:def 6; reconsider y as Element of X by A4; f.(x,y)>=0 by A1,NAGATA_1:29; hence rn>=0 by A5,Def2; end; dom dist(f,x)=X by FUNCT_2:def 1; hence dist(f,x).:A is non empty bounded_below by A3,XXREAL_2:def 9; end; now let xy be set; assume xy in dom f; then consider x,y such that A6: x in X & y in X and A7: [x,y] = xy by ZFMISC_1:def 2; reconsider x,y as Element of X by A6; f.(x,y) >=0 & 0>-1 by A1,NAGATA_1:29; hence f.xy>-1 by A7; end; hence thesis by A2,SEQ_2:def 2; end; theorem Th5: for X be non empty set,f be Function of [:X,X:],REAL st f is_a_pseudometric_of X for A be non empty Subset of X,x be Element of X holds lower_bound(f,A).x>=0 proof let X be non empty set,f be Function of [:X,X:],REAL such that A1: f is_a_pseudometric_of X; let A be non empty Subset of X,x be Element of X; A2: now let rn; assume rn in (dist(f,x)).:A; then consider y such that A3: y in dom dist(f,x) and y in A and A4: rn = dist(f,x).y by FUNCT_1:def 6; dist(f,x).y=f.(x,y) by A3,Def2; hence rn>=0 by A1,A3,A4,NAGATA_1:29; end; X=dom dist(f,x) by FUNCT_2:def 1; then lower_bound ((dist(f,x)).:A)>=0 by A2,SEQ_4:43; hence thesis by Def3; end; theorem Th6: for X be non empty set,f be Function of [:X,X:],REAL st f is_a_pseudometric_of X for A be Subset of X,x be Element of X holds x in A implies lower_bound(f,A).x=0 proof let X be non empty set,f be Function of [:X,X:],REAL such that A1: f is_a_pseudometric_of X; let A be Subset of X,x be Element of X; assume A2: x in A; then reconsider A as non empty Subset of X; A3: dist(f,x).:A is non empty bounded_below by A1,Lm1; f is Reflexive by A1,NAGATA_1:def 10; then f.(x,x)=0 by METRIC_1:def 2; then X=dom dist(f,x) & dist(f,x).x=0 by Def2,FUNCT_2:def 1; then 0 in dist(f,x).:A by A2,FUNCT_1:def 6; then lower_bound(dist(f,x).:A)<=0 by A3,SEQ_4:def 2; then lower_bound(f,A).x <=0 by Def3; hence thesis by A1,Th5; end; theorem Th7: for pmet st pmet is_a_pseudometric_of the carrier of T for x,y be Point of T,A be non empty Subset of T holds abs(lower_bound(pmet,A).x-lower_bound(pmet,A).y)<= pmet.(x,y) proof let pmet such that A1: pmet is_a_pseudometric_of the carrier of T; A2: pmet is symmetric by A1,NAGATA_1:def 10; let x,y be Point of T,A be non empty Subset of T; A3: for x1,y1 be Point of T holds lower_bound(pmet,A).y1-lower_bound(pmet,A).x1>=-pmet.(x1, y1) proof let x1,y1 be Point of T; A4: dist(pmet,x1).:A is non empty bounded_below by A1,Lm1; A5: for rn st rn in dist(pmet,y1).:A holds rn>=lower_bound(dist(pmet,x1).:A)-pmet. (x1,y1) proof let rn; assume rn in dist(pmet,y1).:A; then consider z such that A6: z in dom dist(pmet,y1) and A7: z in A and A8: dist(pmet,y1).z=rn by FUNCT_1:def 6; reconsider z as Point of T by A6; A9: dist(pmet,x1).z= pmet.(x1,z) by Def2; pmet is triangle by A1,NAGATA_1:def 10; then A10: pmet.(x1,y1)+pmet.(y1,z)>=pmet.(x1,z) by METRIC_1:def 5; dom dist(pmet,x1)= the carrier of T by FUNCT_2:def 1; then dist(pmet,x1).z in dist(pmet,x1).:A by A7,FUNCT_1:def 6; then pmet.(x1,z)>=lower_bound(dist(pmet,x1).:A) by A4,A9,SEQ_4:def 2; then pmet.(x1,y1)+pmet.(y1,z)>=lower_bound(dist(pmet,x1).:A)+0 by A10,XXREAL_0:2; then pmet.(y1,z)-0>=lower_bound(dist(pmet,x1).:A)-pmet.(x1,y1) by XREAL_1:21; hence thesis by A8,Def2; end; dist(pmet,y1).:A is non empty bounded_below by A1,Lm1; then lower_bound(dist(pmet,y1).:A)-0>= lower_bound(dist(pmet,x1).:A)-pmet.(x1,y1) by A5,SEQ_4:43; then A11: lower_bound(dist(pmet,y1).:A)-lower_bound(dist(pmet,x1).:A) >=0-pmet.(x1,y1) by XREAL_1:17; lower_bound(dist(pmet,y1).:A)=lower_bound(pmet,A).y1 by Def3; hence thesis by A11,Def3; end; then lower_bound(pmet,A).y-lower_bound(pmet,A).x>=-pmet.(x,y); then -(lower_bound(pmet,A).x-lower_bound(pmet,A).y)>=-pmet.(x,y); then A12: (lower_bound(pmet,A).x-lower_bound(pmet,A).y)<= pmet.(x,y) by XREAL_1:24; lower_bound(pmet,A).x-lower_bound(pmet,A).y>=-pmet.(y,x) by A3; then (lower_bound(pmet,A).x-lower_bound(pmet,A).y)>=-pmet.(x,y) by A2,METRIC_1:def 4; hence thesis by A12,ABSVALUE:5; end; theorem Th8: for pmet st pmet is_a_pseudometric_of the carrier of T & for p holds dist(pmet,p) is continuous for A be non empty Subset of T holds lower_bound(pmet, A) is continuous proof let pmet such that A1: pmet is_a_pseudometric_of the carrier of T and A2: for p holds dist(pmet,p) is continuous; let A be non empty Subset of T; reconsider infR=lower_bound(pmet,A) as Function of T,R^1 by TOPMETR:17; now let t be Point of T; reconsider dR=dist(pmet,t) as Function of T,R^1 by TOPMETR:17; for R being Subset of R^1 st R is open & infR.t in R ex U being Subset of T st U is open & t in U & infR.:U c= R proof reconsider infRt=infR qua real-valued Function.t, dRt=dR qua real-valued Function.t as Point of RealSpace by METRIC_1:def 13; let R be Subset of R^1; assume R is open & infR.t in R; then consider r being real number such that A3: r>0 and A4: Ball(infRt,r) c= R by TOPMETR:15,def 6; reconsider dB=Ball(dRt,r) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17; abs(dR.t-dR.t)=0 by ABSVALUE:2; then dist(dRt,dRt)=0 by A1,NAGATA_1:29; then A11: dR.b>=0 by Def2; dR.t=pmet.(t,t) by Def2; then dR.t=0 by A1,NAGATA_1:28; then A12: dist(dRt,dRb)=abs(0-dR.b) by TOPMETR:11; dom dR=the carrier of T by FUNCT_2:def 1; then dR.b in dR.:B by A9,FUNCT_1:def 6; then dist(dRt,dRb)0 and A9: Ball(xP,r) c= AT by A5,A7,PCOMPS_1:def 4; reconsider xT=x as Element of T by A7; A10: ex y st y in AT` by A6,XBOOLE_0:def 1; reconsider B=Ball(xP,r) as Subset of T by A1,PCOMPS_2:4; set Inf={p where p is Point of T:lower_bound(pmet,B`).p=0}; AT`c=B` by A9,SUBSET_1:12; then consider b be set such that A11: b in B` by A10; B`=Inf proof thus B`c=Inf proof let y such that A12: y in B`; lower_bound(pmet,B`).y=0 by A1,A12,Th6,Th9; hence thesis by A12; end; let y; assume y in Inf; then consider yT be Point of T such that A13: y=yT and A14: lower_bound(pmet,B`).yT=0; assume not y in B`; then A15: yT in B by A13,XBOOLE_0:def 5; reconsider yP=yT as Point of PM by A1,PCOMPS_2:4; pmet is_a_pseudometric_of the carrier of T by A1,Th9; then A16: dist(pmet,yT).:B` is non empty bounded_below by A11,Lm1; Ball(xP,r) in Family_open_set PM by PCOMPS_1:29; then consider s such that A17: s>0 and A18: Ball(yP,s)c=Ball(xP,r) by A15,PCOMPS_1:def 4; lower_bound(dist(pmet,yT).:B`)=0 by A14,Def3; then consider rn such that A19: rn in dist(pmet,yT).:B` and A20: rn<0+s by A17,A16,SEQ_4:def 2; consider z such that A21: z in dom dist(pmet,yT) and A22: z in B` and A23: rn =dist(pmet,yT).z by A19,FUNCT_1:def 6; reconsider zT=z as Point of T by A21; reconsider zP=z as Point of PM by A1,A21,PCOMPS_2:4; pmet.(yT,zT)0 & Ball(xP,r) c= AP proof let xP be Element of PM such that A27: xP in AP; reconsider xT=xP as Element of T by A1,PCOMPS_2:4; take r=lower_bound(pmet,AT`).xT; A28: Ball(xP,r) c= AP proof pmet is_a_pseudometric_of the carrier of T by A1,Th9; then A29: dist(pmet,xT).:AT` is non empty bounded_below by A26,Lm1; let y; assume that A30: y in Ball(xP,r) and A31: not y in AP; reconsider yP=y as Point of PM by A30; A32: dist(xP,yP)0 proof assume lower_bound(pmet,AT`).xT<=0; then lower_bound(pmet,AT`).xT=0 by A1,A26,Th5,Th9; then xT in AT` by A35; then AT` meets AT by A27,XBOOLE_0:3; hence thesis by XBOOLE_1:79; end; hence thesis by A28; end; hence thesis by PCOMPS_1:def 4; end; end; then the topology of T =Family_open_set PM by A4,XBOOLE_0:def 10; hence thesis by A1,PCOMPS_1:def 8; end; theorem Th11: for FS2 st (for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of the carrier of T) & for pq holds FS2#pq is summable for pmet st for pq holds pmet.pq=Sum(FS2#pq) holds pmet is_a_pseudometric_of the carrier of T proof set cT=the carrier of T; let FS2 such that A1: for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of cT and A2: for pq holds FS2#pq is summable; let pmet such that A3: for pq holds pmet.pq=Sum(FS2#pq); now let a,b,c be Point of T; thus pmet.(a,a)=0 proof set aa=[a,a]; set F=FS2#aa; now let n; consider pmet1 such that A4: FS2.n=pmet1 and A5: pmet1 is_a_pseudometric_of cT by A1; pmet1.(a,a)=0 by A5,NAGATA_1:28; hence F.n=0*F.n by A4,SEQFUNC:def 10; end; then A6: F=0(#)F by SEQ_1:9; F is summable by A2; then Sum(F)=0*Sum(F) by A6,SERIES_1:10; hence thesis by A3; end; thus pmet.(a,c)<=pmet.(a,b)+pmet.(c,b) proof set ab=[a,b],cb=[c,b],ac=[a,c]; set Fac=FS2#ac; set Fab=FS2#ab; set Fcb=FS2#cb; A7: now let n; A8: FS2.n.ac= Fac.n & FS2.n.ab=Fab.n by SEQFUNC:def 10; consider pmet1 such that A9: FS2.n=pmet1 and A10: pmet1 is_a_pseudometric_of cT by A1; A11: 0<=pmet1.(a,c) by A10,NAGATA_1:29; pmet1.(a,c)<=pmet1.(a,b)+pmet1.(c,b) by A10,NAGATA_1:28; then Fac.n<=(Fab.n+Fcb.n) by A9,A8,SEQFUNC:def 10; hence 0<=Fac.n & Fac.n<=(Fab+Fcb).n by A9,A11,SEQFUNC:def 10,SEQ_1:7; end; A12: Fab is summable & Fcb is summable by A2; then Fab+Fcb is summable by SERIES_1:7; then A13: Sum(Fac)<=Sum(Fab+Fcb) by A7,SERIES_1:20; A14: Sum(Fab)=pmet.ab & Sum(Fcb)=pmet.cb by A3; Sum(Fab+Fcb)=Sum(Fab)+Sum(Fcb) by A12,SERIES_1:7; hence thesis by A3,A13,A14; end; end; hence thesis by NAGATA_1:28; end; theorem Th12: for n,seq st for m st m<=n holds seq.m<=r for m st m<=n holds Partial_Sums(seq).m <= r * (m+1) proof let n,seq such that A1: for m st m<=n holds seq.m<=r; defpred P[Element of NAT] means $1<=n implies Partial_Sums(seq).$1<=r*($1+1); A2: for m st P[m] holds P[m+1] proof let m such that A3: P[m]; A4: Partial_Sums(seq).(m+1) = Partial_Sums(seq).m+seq.(m+1) by SERIES_1:def 1; assume A5: m+1<=n; then seq.(m+1)<=r by A1; then Partial_Sums(seq).(m+1)<=(r*(m+1)) + r by A3,A5,A4,NAT_1:13,XREAL_1:7; hence thesis; end; Partial_Sums(seq).0=seq.0 by SERIES_1:def 1; then A6: P[ 0 ] by A1; for m holds P[m] from NAT_1:sch 1(A6,A2); hence thesis; end; theorem Th13: for k holds abs(Partial_Sums(seq).k)<=Partial_Sums(abs(seq)).k proof set PS=Partial_Sums(seq),absPS=Partial_Sums(abs(seq)); defpred P[Element of NAT] means abs(PS.$1)<=absPS.$1; A1: for k st P[k] holds P[k+1] proof let k; assume P[k]; then A2: abs(PS.k)+abs(seq.(k+1)) <=absPS.k+abs(seq.(k+1)) by XREAL_1:7; PS.(k+1)=PS.k+seq.(k+1) by SERIES_1:def 1; then A3: abs(PS.(k+1))<=abs(PS.k)+abs(seq.(k+1)) by COMPLEX1:56; (abs seq).(k+1)= abs(seq.(k+1)) by SEQ_1:12; then abs(PS.(k+1))<=absPS.k+(abs seq).(k+1) by A3,A2,XXREAL_0:2; hence thesis by SERIES_1:def 1; end; absPS.0=(abs seq).0 & (abs seq).0=abs(seq.0) by SEQ_1:12,SERIES_1:def 1; then A4: P[ 0 ] by SERIES_1:def 1; for k holds P[k] from NAT_1:sch 1 (A4,A1); hence thesis; end; theorem Th14: for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n ex f st FS1.n=f & f is continuous & for p holds f.p>=0) & (ex seq st seq is summable & for n,p holds (FS1#p).n<=seq.n) for f st for p holds f.p=Sum(FS1# p) holds f is continuous proof let FS1 be Functional_Sequence of the carrier of T,REAL such that A1: for n ex f st FS1.n=f & f is continuous & for p holds f.p>=0 and A2: ex seq st seq is summable & for n,p holds (FS1#p).n<=seq.n; let f such that A3: for p holds f.p=Sum(FS1#p); reconsider fR=f as Function of T,R^1 by TOPMETR:17; now let p; for R being Subset of R^1 st R is open & fR.p in R ex U being Subset of T st U is open & p in U & fR.:U c= R proof reconsider fRp=fR qua real-valued Function.p as Point of RealSpace by METRIC_1:def 13; let R be Subset of R^1; assume R is open & fR.p in R; then consider rn such that A4: rn>0 and A5: Ball(fRp,rn) c= R by TOPMETR:15,def 6; set r2=rn/2,r4=rn/4; reconsider r2,r4 as Real; A6: r4>0 by A4,XREAL_1:224; consider seq such that A7: seq is summable and A8: for n,q holds (FS1#q).n<=seq.n by A2; Partial_Sums(seq) is convergent by A7,SERIES_1:def 2; then consider n such that A9: for m st n<=m holds abs(Partial_Sums(seq).m-lim Partial_Sums( seq))=0 by A1; reconsider f19=f1 as Function of T,R^1 by TOPMETR:17; reconsider f1p=f19 qua real-valued Function.p as Point of RealSpace by METRIC_1:def 13; set B=Ball(f1p,r2/(n+1)); reconsider B as Subset of R^1 by METRIC_1:def 13,TOPMETR:17; dist(f1p,f1p)=0 & r2>0 by A4,METRIC_1:1,XREAL_1:215; then dist(f1p,f1p)=0 proof let k,q; (ex f1 st FS1.k=f1 & f1 is continuous & for q holds f1.q >=0 )& FS1.k.q=( FS1#q).k by A1,SEQFUNC:def 10; hence thesis; end; A18: for k holds (seq^\(n+1)).k>=0 proof let k; 0<=(FS1#p).(n+1+k) & seq.(n+1+k)=(seq^\(n+1)).k by A17,NAT_1:def 3; hence thesis by A8; end; reconsider RNG=rng FSn as Subset-Family of T; A19: RNG is open proof let Q be Subset of T; assume Q in RNG; then consider x such that A20: x in dom FSn and A21: FSn.x=Q by FUNCT_1:def 3; ex SS being Subset of T st SS = FSn.x & SS is open & p in SS & for f1 st FS1.x=f1 for f1p be Point of RealSpace st f1p=f1.p holds f1 .:SS c= Ball( f1p,r2/(n+1)) by A16,A20; hence thesis by A21; end; 0 in {0} by TARSKI:def 1; then 0 in {0}\/Seg(n) by XBOOLE_0:def 3; then reconsider RNG as non empty Subset-Family of T by FUNCT_2:4; A22: lim Partial_Sums( seq ) =Sum(seq) & Sum(seq)=Partial_Sums(seq).n + Sum(seq^\ (n+1)) by A7,SERIES_1:15,def 3; abs(Partial_Sums(seq).n-lim Partial_Sums(seq))=0 by A18,SERIES_1:18; then A24: Sum(seq^\(n+1))=1 by NAT_1:14; then k in {0} or k in Seg n by A34,FINSEQ_1:1,TARSKI:def 1; then A35: k in {0}\/Seg n by XBOOLE_0:def 3; then FSn.k in RNG by FUNCT_2:4; then A36: q in FSn.k by A32,SETFAM_1:def 1; dom (sp-sq)= NAT by FUNCT_2:def 1; then A37: (sp-sq).k=sp.k-sq.k by VALUED_1:13; consider f1 such that A38: FS1.k=f1 and f1 is continuous and for p holds f1.p>=0 by A1; reconsider f1p=f1.p,f1q=f1.q as Point of RealSpace by METRIC_1:def 13 ; ex SS being Subset of T st SS = FSn.k & SS is open & p in SS & for f1 st FS1.k=f1 for f1p be Point of RealSpace st f1p=f1.p holds f1 .:SS c= Ball(f1p,r2/(n+1)) by A16,A35; then A39: f1.:(FSn.k) c= Ball(f1p,r2/(n+1)) by A38; dom f1=the carrier of T by FUNCT_2:def 1; then f1q in f1.:(FSn.k) by A36,FUNCT_1:def 6; then dist(f1p,f1q)0 by NEWTON:83; then A11: Geo.k>0 by PREPOWER:def 1; then (Geo.k)*(pmet1.pq)<=(Geo.k)*s by A8,XREAL_1:64; hence thesis by A6,A5,A10,A9,A11,SEQ_1:9; end; A12: for n ex f be RealMap of [:T,T:] st (GeoF9.n=f & f is continuous & for pq9 holds f.pq9>=0) proof let n; consider pmet1 such that A13: FS2.n=pmet1 and pmet1 is_a_pseudometric_of cT and for pq holds pmet1.pq<=s and A14: for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1; cTT=[:cT,cT:] by BORSUK_1:def 2; then reconsider pmet19=pmet1 as RealMap of [:T,T:]; reconsider pR=pmet19 as Function of [:T,T:],R^1 by TOPMETR:17; pmet19 is continuous by A14; then pR is continuous by JORDAN5A:27; then consider fR be Function of [:T,T:],R^1 such that A15: for pq9 be Point of [:T,T:],rn st pR.pq9=rn holds fR.pq9= (Geo.n) *rn and A16: fR is continuous by JGRAPH_2:23; reconsider f=fR as RealMap of [:T,T:] by TOPMETR:17; A17: dom f=cTT by FUNCT_2:def 1; take f; A18: dom pmet1=[:cT,cT:] by FUNCT_2:def 1; A19: (GeoF9.n)=(Geo.n)(#)FS2.n by A2; then A20: dom (FS2.n)=dom (GeoF9.n) by VALUED_1:def 5; A21: [:cT,cT:]=cTT by BORSUK_1:def 2; A22: now let pq9 such that pq9 in dom (GeoF9.n); (GeoF9.n).pq9=(Geo.n)*pmet1.pq9 by A13,A19,A20,A18,A21,VALUED_1:def 5; hence (GeoF9.n).pq9=f.pq9 by A15; end; now let pq9; reconsider pq=pq9 as Element of [:cT,cT:] by BORSUK_1:def 2; GeoF9.n.pq9=(GeoF#pq).n & (GeoF#pq).n >=0 by A3,SEQFUNC:def 10; hence f.pq9>=0 by A13,A20,A18,A22; end; hence thesis by A13,A16,A20,A18,A17,A21,A22,JORDAN5A:27,PARTFUN1:5; end; let pmet such that A23: for pq holds pmet.pq=Sum(Geo(#)(FS2#pq)); A24: for pq holds pmet.pq=Sum(GeoF#pq) proof let pq; now let z; assume z in NAT; then reconsider k=z as Element of NAT; ex pmet1 st FS2.k=pmet1 & pmet1 is_a_pseudometric_of cT &( for pq holds pmet1.pq<=s)& for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1 ; then dom ((Geo.k)(#)(FS2.k))=[:cT,cT:] by FUNCT_2:def 1; then (Geo.k)*(FS2.k).pq=((Geo.k)(#)(FS2.k)).pq by VALUED_1:def 5 .=GeoF.k.pq by A2 .=(GeoF#pq).k by SEQFUNC:def 10; then (GeoF#pq).k=(Geo.k)*(FS2#pq).k by SEQFUNC:def 10 .=(Geo(#)(FS2#pq)).k by SEQ_1:8; hence (Geo(#)(FS2#pq)).z=(GeoF#pq).z; end; then Geo(#)(FS2#pq)=(GeoF#pq) by FUNCT_2:12; hence thesis by A23; end; A25: for n ex pmet1 st GeoF.n=pmet1 & pmet1 is_a_pseudometric_of cT proof let n; consider pmet1 such that A26: FS2.n=pmet1 and A27: pmet1 is_a_pseudometric_of cT and for pq holds pmet1.pq<=s and for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1; deffunc F(Element of cT,Element of cT)=(Geo.n)*pmet1.($1,$2); consider GF be Function of [:cT,cT:],REAL such that A28: for p for q holds GF.(p,q)=F(p,q) from BINOP_1:sch 4; now let a,b,c be Point of T; (1/2)|^n>0 by NEWTON:83; then A29: ((1/2)GeoSeq.n)>0 by PREPOWER:def 1; pmet1.(a,c)<=pmet1.(a,b)+pmet1.(c,b) by A27,NAGATA_1:28; then pmet1.(a,c)*((1/2)GeoSeq.n)<=(pmet1.(a,b)+ pmet1.(c,b))*(Geo.n) by A29,XREAL_1:64; then A30: GF.(a,c)<=(Geo.n)*pmet1.(a,b)+(Geo.n)*pmet1.(c,b) by A28; GF.(a,a)=(Geo.n)*pmet1.(a,a) & pmet1.(a,a)=0 by A27,A28,NAGATA_1:28; hence GF.(a,a)=0; (Geo.n)*pmet1.(a,b)=GF.(a,b) by A28; hence GF.(a,c)<=GF.(a,b)+GF.(c,b) by A28,A30; end; then A31: GF is_a_pseudometric_of cT by NAGATA_1:28; A32: (GeoF.n)=(Geo.n)(#)FS2.n by A2; then A33: dom (FS2.n)=dom (GeoF.n) by VALUED_1:def 5; A34: now let x,y; assume A35: [x,y] in dom (GeoF.n); then reconsider x9=x,y9=y as Point of T by ZFMISC_1:87; GF.(x9,y9)= (Geo.n)*pmet1.(x9,y9) by A28; hence (GeoF.n).(x,y)=GF.(x,y) by A26,A32,A35,VALUED_1:def 5; end; dom pmet1=[:cT,cT:] & dom GF= [:cT,cT:] by FUNCT_2:def 1; hence thesis by A26,A33,A34,A31,BINOP_1:20; end; (1/2)<1; then abs(1/2)<1 by ABSVALUE:def 1; then A36: Geo is summable by SERIES_1:24; A37: for pq,pq9 st pq=pq9 holds GeoF#pq=GeoF9#pq9 proof let pq,pq9 such that A38: pq=pq9; now let x be Element of NAT; (GeoF#pq).x=GeoF.x.pq by SEQFUNC:def 10; hence (GeoF#pq).x=(GeoF9#pq9).x by A38,SEQFUNC:def 10; end; hence thesis by FUNCT_2:63; end; A39: ex seq st seq is summable & for n,pq9 holds (GeoF9#pq9).n<=seq.n proof take SGeo; thus SGeo is summable by A36,SERIES_1:10; now let n,pq9; reconsider pq=pq9 as Element of [:cT,cT:] by BORSUK_1:def 2; (GeoF9#pq9).n =(GeoF#pq).n by A37; hence (GeoF9#pq9).n <=SGeo.n by A3; end; hence thesis; end; A40: now let pmet19 such that A41: pmet=pmet19; for pq9 holds pmet19.pq9=Sum(GeoF9#pq9) proof let pq9; reconsider pq=pq9 as Element of [:cT,cT:] by BORSUK_1:def 2; pmet.pq=Sum(GeoF#pq) by A24; hence thesis by A37,A41; end; hence pmet19 is continuous by A12,A39,Th14; end; for pq holds GeoF#pq is summable proof let pq; for k holds 0<=(GeoF#pq).k & (GeoF#pq).k<=SGeo.k & SGeo is summable by A3,A36,SERIES_1:10; hence thesis by SERIES_1:20; end; hence thesis by A25,A24,A40,Th11; end; theorem Th16: for pmet st pmet is_a_pseudometric_of the carrier of T & for pmet9 st pmet=pmet9 holds pmet9 is continuous for A be non empty Subset of T,p holds p in Cl A implies lower_bound(pmet,A).p=0 proof set rn=0; let pmet such that A1: pmet is_a_pseudometric_of the carrier of T and A2: for pmet9 st pmet=pmet9 holds pmet9 is continuous; let A be non empty Subset of T,p; A3: dom lower_bound(pmet,A)= the carrier of T by FUNCT_2:def 1; reconsider Z={rn},infA=lower_bound(pmet,A).:A as Subset of R^1 by TOPMETR:17; infA c= Z proof let infa be set; assume infa in infA; then ex a be set st a in dom lower_bound(pmet,A) & a in A & infa=lower_bound (pmet,A).a by FUNCT_1:def 6; then infa=0 by A1,Th6; hence thesis by TARSKI:def 1; end; then A4: Cl (infA) c= Cl Z by PRE_TOPC:19; reconsider InfA=lower_bound(pmet,A) as Function of T,R^1 by TOPMETR:17; for p holds dist(pmet,p) is continuous by A2,Th4; then lower_bound(pmet,A) is continuous by A1,Th8; then InfA is continuous by JORDAN5A:27; then A5: InfA.:(Cl A) c= Cl(InfA.:A) by TOPS_2:45; assume p in Cl A; then A6: lower_bound(pmet,A).p in lower_bound(pmet,A).:(Cl A) by A3,FUNCT_1:def 6; Z is closed by PCOMPS_1:7,TOPMETR:17; then Z=Cl Z by PRE_TOPC:22; then InfA.:(Cl A)c=Z by A4,A5,XBOOLE_1:1; hence thesis by A6,TARSKI:def 1; end; theorem Th17: for T st T is T_1 for s, FS2 st (for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of the carrier of T & (for pq holds pmet.pq<=s) & for pmet9 st pmet=pmet9 holds pmet9 is continuous) & for p,A9 st not p in A9 & A9 is closed ex n st for pmet st FS2.n=pmet holds lower_bound(pmet,A9).p>0 holds (ex pmet st pmet is_metric_of the carrier of T & for pq holds pmet.pq=Sum((1/2)GeoSeq(#) (FS2#pq))) & T is metrizable proof let T such that A1: T is T_1; set cT=the carrier of T,Geo=(1/2)GeoSeq; let s,FS2 such that A2: for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of the carrier of T & (for pq holds pmet.pq<=s) & for pmet9 st pmet=pmet9 holds pmet9 is continuous and A3: for p,A9 st not p in A9 & A9 is closed ex n st for pmet st FS2.n= pmet holds lower_bound(pmet,A9).p>0; deffunc pm(Element of cT,Element of cT)=Sum(Geo(#)(FS2#[$1,$2])); consider pmet such that A4: for p,q holds pmet.(p,q)=pm(p,q) from BINOP_1:sch 4; A5: for pq holds pmet.pq=Sum(Geo(#)(FS2#pq)) proof let pq; consider p,q be set such that A6: p in cT & q in cT and A7: pq=[p,q] by ZFMISC_1:def 2; pmet.pq = pmet.(p,q) by A7; hence thesis by A4,A6,A7; end; A8: for pq,n holds 0<=(Geo(#)(FS2#pq)).n & (Geo(#)(FS2#pq)).n<=(s(#)Geo).n proof let pq,n; consider x,y such that A9: x in cT & y in cT and A10: [x,y]=pq by ZFMISC_1:def 2; reconsider x,y as Point of T by A9; A11: (Geo.n)*s=(s(#)Geo).n by SEQ_1:9; (1/2)|^n>0 by NEWTON:83; then A12: Geo.n>0 by PREPOWER:def 1; consider pmet1 such that A13: FS2.n=pmet1 and A14: pmet1 is_a_pseudometric_of cT and A15: for pq holds pmet1.pq<=s and for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2; A16: 0<=pmet1.(x,y) by A14,NAGATA_1:29; A17: pmet1.pq=(FS2#pq).n by A13,SEQFUNC:def 10; then (Geo.n)*(FS2#pq).n<=(Geo.n)*s by A15,A12,XREAL_1:64; hence thesis by A10,A16,A12,A17,A11,SEQ_1:8; end; A18: for p,q holds pmet.(p,q)=0 implies p=q proof let p,q; assume that A19: pmet.(p,q)=0 and A20: p<>q; set Q={q}; A21: not p in Q by A20,TARSKI:def 1; set pq=[p,q]; A22: Sum(Geo(#)(FS2#pq))=0 by A5,A19; A23: for n holds 0<=(Geo(#)(FS2#pq)).n & (Geo(#)(FS2#pq)).n<=(s(#)Geo).n by A8; Q is closed by A1,URYSOHN1:19; then consider n such that A24: for pmet1 st FS2.n=pmet1 holds lower_bound(pmet1,Q).p>0 by A3,A21; consider pmet1 such that A25: FS2.n=pmet1 and A26: pmet1 is_a_pseudometric_of cT and for pq holds pmet1.pq<=s and for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2; lower_bound(pmet1,Q).p> 0 by A24,A25; then A27: lower_bound(dist(pmet1,p).:Q)>0 by Def3; (1/2)<1; then abs(1/2)<1 by ABSVALUE:def 1; then Geo is summable by SERIES_1:24; then s(#)Geo is summable by SERIES_1:10; then Geo(#)(FS2#pq) is summable by A23,SERIES_1:20; then (Geo(#)(FS2#pq)).n=0 by A23,A22,RSSPACE:17; then A28: Geo.n *(FS2#pq).n=0 by SEQ_1:8; (1/2)|^n>0 by NEWTON:83; then Geo.n<>0 by PREPOWER:def 1; then A29: (FS2#pq).n=0 by A28,XCMPLX_1:6; A30: pmet1.(p,q)=dist(pmet1,p).q by Def2; dom dist(pmet1,p)=cT & q in Q by FUNCT_2:def 1,TARSKI:def 1; then A31: dist(pmet1,p).q in dist(pmet1,p).:Q by FUNCT_1:def 6; dist(pmet1,p).:Q is non empty bounded_below by A26,Lm1; then dist(pmet1,p).q>0 by A31,A27,SEQ_4:def 2; hence thesis by A25,A29,A30,SEQFUNC:def 10; end; pmet is_a_pseudometric_of cT by A2,A5,Th15; then pmet is Reflexive discerning symmetric triangle by A18,METRIC_1:def 3 ,NAGATA_1:def 10; then A32: pmet is_metric_of cT by METRIC_6:3; hence ex pmet st pmet is_metric_of the carrier of T & for pq holds pmet.pq= Sum((1/2)GeoSeq(#)(FS2#pq)) by A5; for A be non empty Subset of T holds Cl A ={p where p is Point of T:lower_bound( pmet,A).p=0} proof let A be non empty Subset of T; set INF={p where p is Point of T:lower_bound(pmet,A).p=0}; A33: INF c= Cl A proof let x; assume x in INF; then consider p be Point of T such that A34: x=p and A35: lower_bound(pmet,A).p=0; A36: lower_bound(dist(pmet,p).:A)=0 by A35,Def3; pmet is_a_pseudometric_of cT by A2,A5,Th15; then A37: dist(pmet,p).:A is non empty bounded_below by Lm1; A38: A c= Cl A & ex y st y in A by PRE_TOPC:18,XBOOLE_0:def 1; A39: A c= Cl A by PRE_TOPC:18; assume not x in Cl A; then consider n such that A40: for pmet1 st FS2.n=pmet1 holds lower_bound(pmet1,Cl A).p>0 by A3,A34,A38; (1/2)|^n>0 by NEWTON:83; then A41: Geo.n>0 by PREPOWER:def 1; (1/2)|^n>0 by NEWTON:83; then A42: Geo.n>0 by PREPOWER:def 1; consider pmet1 such that A43: FS2.n=pmet1 and A44: pmet1 is_a_pseudometric_of cT and for pq holds pmet1.pq<=s and for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2; set r=Geo.n*lower_bound(pmet1,Cl A).p; A45: lower_bound(dist(pmet1,p).:(Cl A))= lower_bound(pmet1,Cl A).p by Def3; A46: lower_bound(pmet1,Cl A).p>0 by A40,A43; then r>0 by A41,XREAL_1:129; then r/2>0 by XREAL_1:215; then consider rn such that A47: rn in dist(pmet,p).:A and A48: rn=(Geo(#)(FS2#pa)).n by A5,A56; then (Geo(#)(FS2#pa)).n =1 & len p>len q) holds ex r be FinSequence of D st r is one-to-one & rng r=rng p \rng q & B "**" p =B.(B "**" q,B "**" r) proof let D be non empty set, p,q be FinSequence of D,B be BinOp of D such that A1: p is one-to-one and A2: q is one-to-one and A3: rng q c= rng p and A4: B is commutative associative and A5: B is having_a_unity or len q>=1 & len p>len q; A6: card (rng p)=len p by A1,FINSEQ_4:62; consider r be FinSequence such that A7: rng r=rng p \rng q and A8: r is one-to-one by FINSEQ_4:58; reconsider r as FinSequence of D by A7,FINSEQ_1:def 4; rng (q^r)=rng q \/(rng p\ rng q ) by A7,FINSEQ_1:31; then A9: rng (q^r)=rng p by A3,XBOOLE_1:45; rng r misses rng q by A7,XBOOLE_1:79; then A10: q^r is one-to-one by A2,A8,FINSEQ_3:91; then card (rng (q^r))=len (q^r) by FINSEQ_4:62; then len q < len q+ len r or B is having_a_unity by A5,A9,A6,FINSEQ_1:22; then A11: 1<=len r& 1<=len q & 1<=len p or B is having_a_unity by A5,NAT_1:19 ,XXREAL_0:2; ex P be Permutation of dom p st p*P=(q^r) & dom P = dom p & rng P = dom p by A1,A10,A9,BHSP_5:1; then A12: B "**" p= B "**" (q^r) by A4,A11,FINSOP_1:7; B "**" (q ^ r) = B.(B "**" q,B "**" r) by A4,A11,FINSOP_1:5; hence thesis by A7,A8,A12; end; registration let T1,T2 be TopSpace; let f be RealMap of [:T1,T2:]; let t1 be Point of T1, t2 be Point of T2; cluster f.(t1,t2) -> real; coherence; end; Lm2: PairFunc" = PairFunc qua Function" by Th2,TOPS_2:def 4; ::$N Nagata-Smirnov Theorem theorem Th19: for T holds (T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite) iff T is metrizable proof let T; 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 proof 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 be FamilySequence of T st Bn is Basis_sigma_locally_finite; set Fun=Funcs(cTT,REAL); consider Bn be FamilySequence of T such that A4: Bn is Basis_sigma_locally_finite by A3; defpred NN[set,set,RealMap of [:T,T:]] means ex pmet st $3=pmet & $3 is continuous & pmet is_a_pseudometric_of cT & for p,q holds pmet.[p,q]<=1 & for p ,q st ex A,B 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 N[set,set] means ex F be RealMap of [:T,T:] st F = $2 & for n,m st PairFunc".$1=[n,m] holds NN[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 ex pmet9 st NN[n,m,pmet9] proof defpred add9[Element of Fun,Element of Fun,set] means $1+$2=$3; defpred funcdist[RealMap of T,Function] means for p,q holds $2.(p,q)=abs ($1.p-$1.q); let n,m; deffunc V(set)=union{Q where Q is Subset of T: Q in Bn.m & Cl Q c=$1}; set Bnn = Bn.n; deffunc s(Subset of T)={Q where Q is Subset of T: Q in Bn.n& Q meets $1}; defpred S[set,Subset of T] means $1 in $2 & $2 is open & s($2) is finite; A8: for A be set st A in bcT holds V(A) in bcT proof let A be set such that A in bcT; set Um={Q where Q is Subset of T:Q in Bn.m & Cl Q c=A}; now let uv be set; assume uv in V(A); then consider v be set such that A9: uv in v and A10: v in Um by TARSKI:def 4; ex B st v=B & B in Bn.m & Cl B c=A by A10; hence uv in cT by A9; end; then V(A) c= cT by TARSKI:def 3; hence thesis; end; consider Vm be Function of bcT,bcT such that A11: for A be set st A in bcT holds Vm.A=V(A) from FUNCT_2:sch 2(A8 ); defpred F[set,set] means ex F be RealMap of T, S be Subset of T st S = $1 & F = $2 & F is continuous & (for p holds 0 <= F.p & F.p <= 1 & (p in S` implies F.p = 0) & (p in Cl (Vm.S) implies F.p = 1)); A12: Bn.m is locally_finite by A6,NAGATA_1:def 3; A13: for A holds Cl (Vm.A) c=A proof let A; set VmA={Q where Q is Subset of T:Q in Bn.m & Cl Q c=A}; VmA c= bcT proof let B be set; assume B in VmA; then ex C st B=C & C in Bn.m & Cl C c=A; hence thesis; end; then reconsider VmA as Subset-Family of T; A14: union clf VmA c= A proof let ClBu be set; assume ClBu in union clf VmA; then consider ClB be set such that A15: ClBu in ClB and A16: ClB in clf VmA by TARSKI:def 4; reconsider ClB as Subset of T by A16; consider B such that A17: Cl B =ClB and A18: B in VmA by A16,PCOMPS_1:def 2; ex C st B=C & C in Bn.m & Cl C c=A by A18; hence thesis by A15,A17; end; VmA c=Bn.m proof let B be set; assume B in VmA; then ex C st B=C & C in Bn.m & Cl C c=A; hence thesis; end; then Cl union VmA = union clf VmA by A12,PCOMPS_1:9,20; hence thesis by A11,A14; end; A19: for A be set st A in Bnn ex f be set st f in Funcs(cT,REAL) & F[A,f ] proof let A be set; assume A in Bnn; then A20: A in Union Bn by PROB_1:12; Union Bn c= the topology of T by A5,TOPS_2:64; then reconsider A as open Subset of T by A20,PRE_TOPC:def 2; A` misses A by XBOOLE_1:79; then A21: A` misses Cl (Vm.A) by A13,XBOOLE_1:63; T is normal by A1,A4,NAGATA_1:20; then consider f be Function of T,R^1 such that A22: f is continuous & for p holds 0 <= f.p & f.p <= 1 & (p in A` implies f.p=0)& (p in Cl (Vm.A) implies f.p=1) by A21,URYSOHN3:20; reconsider f9=f as RealMap of T by TOPMETR:17; A23: ex F be RealMap of T, S be Subset of T st S = A & F = f9 & F is continuous & for p holds 0 <= F.p & F.p <= 1 & (p in S` implies F.p = 0) & (p in Cl (Vm.S) implies F.p = 1) proof take f9, A; thus thesis by A22,JORDAN5A:27; end; f9 in Funcs(cT,REAL) by FUNCT_2:8; hence thesis by A23; end; consider Fn be Function of Bnn,Funcs(cT,REAL) such that A24: for A be set st A in Bnn holds F[A,Fn.A] from FUNCT_2:sch 1(A19 ); Bn.n is locally_finite by A6,NAGATA_1:def 3; then A25: for p being Element of cT ex A be Element of bcT st S[p,A] by PCOMPS_1:def 1; consider Sx be Function of cT,bcT such that A26: for p be Element of cT holds S[p,Sx.p] from FUNCT_2:sch 3(A25); defpred ss[set,set] means for x,y be Element of T st $1=[x,y] holds $2= [:Sx.x,Sx.y:]; A27: for pq9 be set st pq9 in cTT ex SS be set st SS in bool cTT & ss[ pq9,SS] proof let pq9 be set; assume pq9 in cTT; then pq9 in [:cT,cT:] by BORSUK_1:def 2; then consider p,q be set such that A28: p in cT & q in cT and A29: pq9=[p,q] by ZFMISC_1:def 2; reconsider p,q as Point of T by A28; now let p1,q1 be Point of T; assume A30: pq9=[p1,q1]; then p1=p by A29,XTUPLE_0:1; hence [:Sx.p,Sx.q:]=[:Sx.p1,Sx.q1:] by A29,A30,XTUPLE_0:1; end; hence thesis; end; consider SS be Function of cTT,bool cTT such that A31: for pq be set st pq in cTT holds ss[pq,SS.pq] from FUNCT_2:sch 1(A27); A32: for pq9 holds pq9 in SS.pq9 & SS.pq9 is open proof let pq9 be Point of [:T,T:]; pq9 in cTT; then pq9 in [:cT,cT:] by BORSUK_1:def 2; then consider p,q be set such that A33: p in cT & q in cT and A34: pq9=[p,q] by ZFMISC_1:def 2; reconsider p,q as Point of T by A33; A35: p in Sx.p & q in Sx.q by A26; A36: Sx.p is open & Sx.q is open by A26; SS.pq9=[:Sx.p,Sx.q:] by A31,A34; hence thesis by A34,A35,A36,BORSUK_1:6,ZFMISC_1:def 2; end; A37: for f,g be Element of Fun ex fg be Element of Fun st add9[f,g,fg] proof let f,g be Element of Fun; set f9=f,g9=g; f9+g9 in Fun by FUNCT_2:8; hence thesis; end; consider ADD be BinOp of Funcs(the carrier of [:T,T:],REAL) such that A38: for f,g be Element of Fun holds add9[f,g,ADD.(f,g)] from BINOP_1:sch 3(A37); A39: for f be Element of Funcs(cT,REAL) ex fxy be Element of Fun st funcdist[f,fxy] proof let f be Element of Funcs(cT,REAL); defpred fd[Element of T,Element of T,set] means $3=abs(f.$1-f.$2); A40: for x,y be Element of cT ex r be Element of REAL st fd[x,y,r]; consider Fd be Function of [:cT,cT:],REAL such that A41: for x,y be Element of cT holds fd[x,y,Fd.(x,y)] from BINOP_1: sch 3(A40); [:cT,cT:]= cTT by BORSUK_1:def 2; then Fd in Fun by FUNCT_2:8; hence thesis by A41; end; consider Fdist be Function of Funcs(cT,REAL),Fun such that A42: for fd be Element of Funcs(cT,REAL) holds funcdist[fd,Fdist.fd] from FUNCT_2:sch 3(A39); deffunc Fx(Element of T)= {Fn.A where A is Subset of T:A in Bn.n & A in s(Sx.$1)}; deffunc RNG(set)={Fdist.fd where fd is RealMap of T:fd in $1}; defpred gxy[set,Function] means $2 is one-to-one & ex p,q st [p,q]=$1 & rng $2=RNG(Fx(p)\/Fx(q)); A43: for p holds Fx(p) is finite proof deffunc Fxx(Subset of T)=Fn.$1; let p; set SFxx={Fxx(A) where A is Subset of T:A in s(Sx.p)}; A44: Fx(p) c= SFxx proof let FA be set; assume FA in Fx(p); then ex A st FA=Fn.A & A in Bn.n & A in s(Sx.p); hence thesis; end; A45: s(Sx.p) is finite by A26; SFxx is finite from FRAENKEL:sch 21(A45); hence thesis by A44; end; A46: for p,q holds RNG(Fx(p)\/Fx(q)) is finite & RNG(Fx(p)\/Fx(q))c=Fun proof deffunc FD(RealMap of T)=Fdist.$1; let p,q; A47: RNG(Fx(p)\/Fx(q)) c=Fun proof let FDm be set; assume FDm in RNG(Fx(p)\/Fx(q)); then consider fd be RealMap of T such that A48: FDm=Fdist.fd and fd in Fx(p)\/Fx(q); fd in Funcs(cT,REAL) by FUNCT_2:8; hence thesis by A48,FUNCT_2:5; end; set RNG9={FD(fd) where fd is Element of Funcs(cT,REAL): fd in Fx(p)\/ Fx(q)}; A49: RNG(Fx(p)\/Fx(q))c=RNG9 proof let Fdistfd be set; assume Fdistfd in RNG(Fx(p)\/Fx(q)); then consider fd be RealMap of T such that A50: Fdistfd =Fdist.fd & fd in Fx(p)\/Fx(q); fd in Funcs(cT,REAL) by FUNCT_2:8; hence thesis by A50; end; Fx(p) is finite & Fx(q) is finite by A43; then A51: Fx(p)\/Fx(q) is finite; RNG9 is finite from FRAENKEL:sch 21(A51); hence thesis by A47,A49; end; A52: for pq be Element of cTT ex G be Element of Fun* st gxy[pq,G] proof let pq be Element of cTT; pq in the carrier of [:T,T:]; then pq in [:cT,cT:] by BORSUK_1:def 2; then consider p,q be set such that A53: p in cT & q in cT and A54: pq=[p,q] by ZFMISC_1:def 2; reconsider p,q as Point of T by A53; consider SF be FinSequence such that A55: rng SF =RNG(Fx(p)\/Fx(q)) and A56: SF is one-to-one by A46,FINSEQ_4:58; rng SF c=Fun by A46,A55; then reconsider SF as FinSequence of Fun by FINSEQ_1:def 4; SF in Fun* by FINSEQ_1:def 11; hence thesis by A54,A55,A56; end; consider SFdist be Function of cTT,Fun* such that A57: for pq be Element of cTT holds gxy[pq,SFdist.pq] from FUNCT_2: sch 3(A52); defpred SFdist[set,set] means for FS be FinSequence of Fun st FS=SFdist. $1 holds $2= ADD "**" FS; A58: for pq be set st pq in cTT ex S be set st S in Fun & SFdist[pq,S] proof let pq be set; assume pq in cTT; then SFdist.pq in Fun* by FUNCT_2:5; then reconsider SF=SFdist.pq as FinSequence of Fun by FINSEQ_1:def 11; for FS be FinSequence of Funcs(cTT,REAL) st FS=SFdist.pq holds ADD "**" FS = ADD "**" SF; hence thesis; end; consider SumFdist be Function of cTT,Funcs(cTT,REAL) such that A59: for xy be set st xy in cTT holds SFdist[xy,SumFdist.xy] from FUNCT_2:sch 1(A58); reconsider SumFdist9=SumFdist as Function of cTT,Funcs(cTT,the carrier of R^1) by TOPMETR:17; reconsider SumFTS9=SumFdist9 Toler as RealMap of [:T,T:] by TOPMETR:17; cTT=[:cT,cT:] by BORSUK_1:def 2; then reconsider SumFTS = SumFdist9 Toler as Function of [:cT,cT:],REAL by TOPMETR:17; A60: for f1,f2 be RealMap of [:T,T:] holds ADD.(f1,f2)=f1+f2 proof let f1,f2 be RealMap of [:T,T:]; reconsider f19=f1,f29=f2 as Element of Fun by FUNCT_2:8; ADD.(f19,f29)=f19+f29 by A38; hence thesis; end; A61: for p,q st ex A,B st A is open & B is open & A in Bn.m & B in Bn.n & p in A & Cl A c= B & not q in B holds SumFTS9.[p,q] >= 1 proof let p,q; assume ex A,B 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; then consider A,B such that A is open and B is open and A62: A in Bn.m and A63: B in Bn.n and A64: p in A and A65: Cl A c= B and A66: not q in B; A67: F[B,Fn.B] by A24,A63; A in {Q where Q is Subset of T:Q in Bn.m & Cl Q c=B} by A62,A65; then A c=V(B) by ZFMISC_1:74; then A68: A c= Vm.B by A11; Vm.B c= Cl(Vm.B) by PRE_TOPC:18; then A69: p in Cl(Vm.B) by A64,A68,TARSKI:def 3; Cl(Vm.B)c=B & p in Sx.p by A13,A26; then Sx.p meets B by A69,XBOOLE_0:3; then A70: B in s(Sx.p) by A63; reconsider pq=[p,q] as Point of [:T,T:] by BORSUK_1:def 2; reconsider SF=SFdist.pq as FinSequence of Fun by FINSEQ_1:def 11; consider x,y be Point of T such that A71: [x,y]=pq and A72: rng SF=RNG(Fx(x)\/Fx(y)) by A57; reconsider ASF=ADD"**"SF as RealMap of [:T,T:] by FUNCT_2:66; assume A73: SumFTS9.[p,q] < 1; reconsider FnB=Fn.B as RealMap of T by A63,FUNCT_2:5,66; A74: FnB in Funcs(cT,REAL) by A63,FUNCT_2:5; q in B` by A66,XBOOLE_0:def 5; then A75: FnB.q=0 by A67; x=p by A71,XTUPLE_0:1; then FnB in Fx(x) by A63,A70; then FnB in Fx(x)\/Fx(y) by XBOOLE_0:def 3; then A76: Fdist.FnB in rng SF by A72; then reconsider FdistFnB=Fdist.FnB as RealMap of [:T,T:] by FUNCT_2:66 ; SF<>{} by A76,RELAT_1:38; then len SF >=1 by NAT_1:14; then consider F be Function of NAT,Fun such that A77: F.1 = SF.1 and A78: for n st 0 <> n & n < len SF holds F.(n+1)=ADD.(F.n,SF.(n+1) ) and A79: ADD"**"SF=F.(len SF) by FINSOP_1:def 1; A80: SumFTS.pq=SumFdist.pq.pq & SumFdist.pq=ASF by A59,NAGATA_1:def 8; defpred P[Element of NAT] means for k st k<>0 & k<=$1 & $1<=len SF for fk,Fn be RealMap of [:T,T:] st fk=SF.k & Fn=F.$1 holds fk.pq<=Fn.pq; A81: for k st k <>0 & k <=len SF for f be RealMap of [:T,T:] st f=SF. k holds f.pq>=0 proof let k such that A82: k <>0 and A83: k <=len SF; k >=1 by A82,NAT_1:14; then k in dom SF by A83,FINSEQ_3:25; then SF.k in RNG(Fx(x)\/Fx(y)) by A72,FUNCT_1:def 3; then consider fd be RealMap of T such that A84: Fdist.fd =SF.k and fd in Fx(x)\/Fx(y); let f be RealMap of [:T,T:] such that A85: f=SF.k; fd in Funcs(cT,REAL) by FUNCT_2:8; then f.(p,q)=abs(fd.p-fd.q) by A42,A85,A84; hence thesis by COMPLEX1:46; end; A86: for i holds P[i] implies P[i+1] proof let i; assume A87: P[i]; let k such that A88: k<>0 and A89: k<=i+1 and A90: i+1<=len SF; now 1<=i+1 by NAT_1:14; then i+1 in dom SF by A90,FINSEQ_3:25; then SF.(i+1) in rng SF by FUNCT_1:def 3; then reconsider SFi1=SF.(i+1) as RealMap of [:T,T:] by FUNCT_2:66; reconsider Fi=F.i as RealMap of [:T,T:] by FUNCT_2:66; let fk,Fn be RealMap of [:T,T:] such that A91: fk=SF.k and A92: Fn=F.(i+1); per cases by A89,XXREAL_0:1; suppose A93: k0 by A88,A93,NAT_1:13; then F.(i+1)=ADD.(F.i,SF.(i+1)) by A78,A94; then A95: Fn =Fi+SFi1 by A60,A92; SFi1.pq>=0 by A81,A90; then Fi.pq +0 <= Fi.pq + SFi1.pq by XREAL_1:7; then A96: Fn.pq>=Fi.pq by A95,NAGATA_1:def 7; A97: i<=len SF by A90,NAT_1:13; k<=i by A93,NAT_1:13; then fk.pq<=Fi.pq by A87,A88,A91,A97; hence fk.pq<=Fn.pq by A96,XXREAL_0:2; end; suppose A98: k=i+1; per cases; suppose i=0; hence fk.pq<=Fn.pq by A77,A91,A92,A98; end; suppose A99: i<>0; i+0=0+fk.pq by XREAL_1:7; F.(i+1)=ADD.(F.i,SF.(i+1)) by A78,A99,A100; then Fn=Fi+fk by A60,A91,A92,A98; hence fk.pq<=Fn.pq by A101,NAGATA_1:def 7; end; end; end; hence thesis; end; A102: P[ 0 ]; A103: for i holds P[i] from NAT_1:sch 1(A102,A86); consider k be set such that A104: k in dom SF and A105: SF.k=Fdist.FnB by A76,FUNCT_1:def 3; A106: k in Seg(len SF) by A104,FINSEQ_1:def 3; FnB.p =1 by A69,A67; then A107: FdistFnB.(p,q)=abs(1-0) by A42,A74,A75; reconsider k as Element of NAT by A104; A108: abs(1)=1 by ABSVALUE:def 1; k<>0 & k <=len SF by A106,FINSEQ_1:1; hence thesis by A73,A80,A79,A103,A107,A108,A105; end; A109: now let p,q; assume ex A,B 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; then SumFTS9.[p,q]>=1 by A61; then A110: 1 = min(1,SumFTS9.[p,q]) by XXREAL_0:def 9; [:cT,cT:]=cTT by BORSUK_1:def 2; hence 1=min(1,SumFTS9).[p,q] by A110,NAGATA_1:def 9; end; A111: for pq be Element of cTT, map9 be Element of Fun st map9 is_a_unity_wrt ADD holds map9.pq=0 proof let pq be Element of cTT, map9 be Element of Fun; assume map9 is_a_unity_wrt ADD; then ADD.(map9,map9)=map9 by BINOP_1:3; then (map9+map9).pq=map9.pq by A38; then map9.pq+map9.pq=map9.pq by NAGATA_1:def 7; hence thesis; end; A112: for pq1,pq2 be Point of [:T,T:] holds (pq1 in SS.pq2 implies SumFdist.pq1.pq1 = SumFdist.pq2.pq1) & for SumFdist1,SumFdist2 be RealMap of [: T,T:] st SumFdist1=SumFdist.pq1 & SumFdist2 = SumFdist.pq2 holds SumFdist1.pq1 >= SumFdist2.pq1 proof deffunc No0(Element of T,Element of T)= {Fn.A where A is Subset of T:A in Bn.n & for FnA be RealMap of T st Fn.A=FnA holds (FnA.$1 > 0 or FnA.$2 > 0)} ; let pq1,pq2 be Point of [:T,T:]; reconsider S1=SFdist.pq1,S2=SFdist.pq2 as FinSequence of Fun by FINSEQ_1:def 11; consider p1,q1 be Point of T such that A113: [p1,q1]=pq1 and A114: rng S1=RNG(Fx(p1)\/Fx(q1)) by A57; A115: for p,q,p1,q1 be Point of T st [p,q] in SS.[p1,q1] holds No0(p,q ) c= Fx(p1)\/Fx(q1) proof let p,q,p1,q1 be Point of T such that A116: [p,q] in SS.[p1,q1]; reconsider pq1=[p1,q1] as Element of cTT by BORSUK_1:def 2; [:Sx.p1,Sx.q1:]=SS.pq1 by A31; then A117: p in Sx.p1 & q in Sx.q1 by A116,ZFMISC_1:87; let no0 be set; assume no0 in No0(p,q); then consider A be Subset of T such that A118: no0=Fn.A and A119: A in Bn.n and A120: for FnA be RealMap of T st Fn.A=FnA holds (FnA.p > 0 or FnA.q > 0); reconsider FnA=Fn.A as RealMap of T by A119,FUNCT_2:5,66; A121: FnA.p > 0 or FnA.q > 0 by A120; F[A,Fn.A] by A24,A119; then not p in cT\A or not q in cT\A by A121; then p in A or q in A by XBOOLE_0:def 5; then A meets Sx.p1 or A meets Sx.q1 by A117,XBOOLE_0:3; then A in s(Sx.p1) or A in s(Sx.q1) by A119; then FnA in Fx(p1) or FnA in Fx(q1) by A119; hence thesis by A118,XBOOLE_0:def 3; end; A122: RNG(No0(p1,q1))c=RNG(Fx(p1)\/Fx(q1)) proof p1 in Sx.p1 & q1 in Sx.q1 by A26; then [p1,q1] in [:Sx.p1,Sx.q1:] by ZFMISC_1:87; then [p1,q1] in SS.[p1,q1] by A31; then A123: No0(p1,q1)c= Fx(p1)\/Fx(q1) by A115; let FD be set; assume FD in RNG(No0(p1,q1)); then ex fd be RealMap of T st FD=Fdist.fd & fd in (No0(p1,q1) ); hence thesis by A123; end; A124: for f be FinSequence of Funcs(cTT,REAL),p,q,p1,q1 be Point of T st rng f= RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q)) holds (ADD "**" f).[p,q]=0 proof let f be FinSequence of Funcs(cTT,REAL),p,q,p1,q1 be Point of T such that A125: rng f= RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q)); reconsider pq=[p,q] as Element of cTT by BORSUK_1:def 2; now per cases; suppose A126: len f = 0; A127: ADD is having_a_unity by A60,NAGATA_1:23; then A128: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2; ADD "**" f=the_unity_wrt ADD by A126,A127,FINSOP_1:def 1; then ADD"**"f is_a_unity_wrt ADD by A128,BINOP_1:def 8; hence (ADD"**"f).pq=0 by A111; end; suppose A129: len f<>0; then len f >=1 by NAT_1:14; then consider F be Function of NAT,Fun such that A130: F.1 = f.1 and A131: for n st 0 <> n & n < len f holds F.(n + 1) = ADD.(F.n ,f.(n + 1)) and A132: ADD"**"f = F.(len f) by FINSOP_1:def 1; defpred R[Element of NAT] means $1<>0 & $1<=len f implies F.$1. pq=0; A133: for k holds R[k] implies R[k+1] proof let k; assume A134: R[k]; assume that k+1<>0 and A135: k+1 <=len f; A136: k< len f by A135,NAT_1:13; k+1>=1 by NAT_1:14; then k+1 in dom f by A135,FINSEQ_3:25; then A137: f.(k+1) in RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q)) by A125, FUNCT_1:def 3; then f.(k+1) in RNG(Fx(p1)\/Fx(q1)); then consider fd be RealMap of T such that A138: Fdist.fd =f.(k+1) and A139: fd in Fx(p1)\/Fx(q1); fd in Funcs(cT,REAL) by FUNCT_2:8; then reconsider Fdistfd=Fdist.fd,Fk1=F.(k+1), Fk=F.k,fk1=f.(k+1) as RealMap of [:T,T:] by A138,FUNCT_2:5,66; fd in Funcs(cT,REAL) by FUNCT_2:8; then A140: Fdistfd.(p,q)=abs(fd.p- fd.q) by A42; A141: not f.(k+1) in RNG(No0(p,q)) by A137,XBOOLE_0:def 5; A142: fd.p=0 & fd.q=0 proof assume A143: fd.p<>0 or fd.q<>0; per cases by A139,XBOOLE_0:def 3; suppose fd in Fx(p1); then consider A be Subset of T such that A144: fd=Fn.A and A145: A in Bn.n and A in s(Sx.p1); A146: F[A,Fn.A] by A24,A145; not fd in No0(p,q) by A141,A138; then ex FnA be RealMap of T st Fn.A=FnA &( not FnA.p > 0)& not FnA.q > 0 by A144,A145; hence contradiction by A143,A144,A146; end; suppose fd in Fx(q1); then consider A be Subset of T such that A147: fd=Fn.A and A148: A in Bn.n and A in s(Sx.q1); A149: F[A,Fn.A] by A24,A148; not fd in No0(p,q) by A141,A138; then ex FnA be RealMap of T st Fn.A=FnA &( not FnA.p > 0)& not FnA.q > 0 by A147,A148; hence contradiction by A143,A147,A149; end; end; per cases; suppose k=0; hence thesis by A130,A138,A142,A140,ABSVALUE:2; end; suppose A150: k>0; then Fk1=ADD.(Fk,fk1) by A131,A136; then Fk1=Fk+fk1 by A60; then Fk1.pq=0+fk1.pq by A134,A135,A150,NAGATA_1:def 7 ,NAT_1:13; hence thesis by A138,A142,A140,ABSVALUE:2; end; end; A151: R[ 0 ]; for n holds R[n] from NAT_1:sch 1(A151,A133); hence (ADD"**"f).pq=0 by A129,A132; end; end; hence thesis; end; A152: RNG(Fx(p1)\/Fx(q1)) is finite by A46; then consider No be FinSequence such that A153: rng No =RNG(No0(p1,q1)) and A154: No is one-to-one by A122,FINSEQ_4:58; RNG(Fx(p1)\/Fx(q1))c=Fun by A46; then A155: RNG(No0(p1,q1)) c= Fun by A122,XBOOLE_1:1; then reconsider No as FinSequence of Fun by A153,FINSEQ_1:def 4; consider p2,q2 be Point of T such that A156: [p2,q2]=pq2 and A157: rng S2=RNG(Fx(p2)\/Fx(q2)) by A57; reconsider S1=SFdist.pq1,S2=SFdist.pq2 as FinSequence of Fun by FINSEQ_1:def 11; set RNiS2=RNG(No0(p1,q1))/\RNG(Fx(p2)\/Fx(q2)); A158: S2 is one-to-one by A57; A159: ADD is having_a_unity & ADD is commutative associative by A60, NAGATA_1:23; S1 is one-to-one by A57; then consider S1No be FinSequence of Fun such that S1No is one-to-one and A160: rng S1No=rng S1 \rng No and A161: ADD"**"S1 =ADD.(ADD"**"No,ADD"**"S1No) by A114,A122,A153,A154,A159,Th18 ; consider NoiS2 be FinSequence such that A162: rng NoiS2 =RNiS2 and A163: NoiS2 is one-to-one by A122,A152,FINSEQ_4:58; RNiS2 c=RNG(No0(p1,q1)) by XBOOLE_1:17; then RNiS2 c= Fun by A155,XBOOLE_1:1; then reconsider NoiS2 as FinSequence of Fun by A162,FINSEQ_1:def 4; rng NoiS2 c= rng No by A153,A162,XBOOLE_1:17; then consider NoNoiS2 be FinSequence of Fun such that NoNoiS2 is one-to-one and A164: rng NoNoiS2=rng No \rng NoiS2 and A165: ADD"**"No=ADD.(ADD"**"NoiS2,ADD"**"NoNoiS2) by A154,A159,A163,Th18; rng NoiS2 c= rng S2 by A157,A162,XBOOLE_1:17; then consider S2No be FinSequence of Fun such that S2No is one-to-one and A166: rng S2No=rng S2 \rng NoiS2 and A167: ADD"**"S2=ADD.(ADD"**"NoiS2,ADD"**"S2No) by A159,A163,A158,Th18; reconsider ANoNoiS2=ADD"**"NoNoiS2,ANo=ADD"**"No,AS1No=ADD"**"S1No, AS2No=ADD"**"S2No,ANoiS2=ADD"**"NoiS2,AS1=ADD"**"S1,AS2=ADD"**"S2 as RealMap of [:T,T:] by FUNCT_2:66; rng S2No= RNG(Fx(p2)\/Fx(q2))\RNG(No0(p1,q1)) by A157,A162,A166, XBOOLE_1:47; then A168: AS2No.pq1=0 by A124,A113; ANo=ANoiS2+ANoNoiS2 by A60,A165; then A169: ANo.pq1=ANoiS2.pq1+ANoNoiS2. pq1 by NAGATA_1:def 7; AS1=ANo+AS1No by A60,A161; then A170: AS1.pq1=ANo.pq1+AS1No.pq1 by NAGATA_1:def 7; AS2=ANoiS2+AS2No by A60,A167; then A171: AS2.pq1=ANoiS2.pq1+AS2No.pq1 by NAGATA_1:def 7; A172: AS1No.pq1=0 by A124,A113,A114,A153,A160; thus pq1 in SS.pq2 implies SumFdist.pq1.pq1 = SumFdist.pq2.pq1 proof A173: ADD is having_a_unity by A60,NAGATA_1:23; then A174: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2; assume A175: pq1 in SS.pq2; now let FD be set; assume FD in RNG (No0(p1,q1)); then A176: ex fd be RealMap of T st FD=Fdist.fd & fd in (No0(p1,q1) ); No0(p1,q1) c= Fx(p2)\/Fx(q2) by A115,A113,A156,A175; hence FD in RNG(Fx(p2)\/Fx(q2)) by A176; end; then RNG (No0(p1,q1)) c= RNG(Fx(p2)\/Fx(q2)) by TARSKI:def 3; then RNiS2=RNG(No0(p1,q1)) by XBOOLE_1:28; then rng NoNoiS2={} by A153,A162,A164,XBOOLE_1:37; then NoNoiS2={} by RELAT_1:41; then len NoNoiS2 =0; then ADD"**"NoNoiS2=the_unity_wrt ADD by A173,FINSOP_1:def 1; then ADD"**"NoNoiS2 is_a_unity_wrt ADD by A174,BINOP_1:def 8; then A177: AS1.pq1=AS2.pq1 by A111,A170,A169,A171,A172,A168; SumFdist.pq1=AS1 by A59; hence thesis by A59,A177; end; A178: ANoNoiS2.(p1,q1)>=0 proof set N=NoNoiS2; per cases; suppose A179: len N=0; A180: ADD is having_a_unity by A60,NAGATA_1:23; then A181: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2; ADD "**" N=the_unity_wrt ADD by A179,A180,FINSOP_1:def 1; then ADD"**"N is_a_unity_wrt ADD by A181,BINOP_1:def 8; hence thesis by A111,A113; end; suppose A182: len N<>0; then len N >=1 by NAT_1:14; then consider F be Function of NAT,Fun such that A183: F.1 = N.1 and A184: for n st 0 <> n & n < len N holds F.(n + 1) = ADD.(F.n,N .(n + 1)) and A185: ADD "**" N=F.(len N) by FINSOP_1:def 1; defpred R[Element of NAT] means $1<>0 & $1<=len N implies for Fn be RealMap of [:T,T:] st Fn=F.$1 holds Fn.(p1,q1)>=0; A186: for k holds R[k] implies R[k+1] proof let k; assume A187: R[k]; assume that k+1<>0 and A188: k+1 <=len N; A189: k< len N by A188,NAT_1:13; k+1>=1 by NAT_1:14; then k+1 in dom N by A188,FINSEQ_3:25; then N.(k+1) in rng No \rng NoiS2 by A164,FUNCT_1:def 3; then N.(k+1) in RNG(No0(p1,q1)) by A153,XBOOLE_0:def 5; then consider fd be RealMap of T such that A190: Fdist.fd =N.(k+1) and fd in No0(p1,q1); fd in Funcs(cT,REAL) by FUNCT_2:8; then reconsider Fdistfd=Fdist.fd,Fk1=F.(k+1), Fk=F.k,Nk1=N.(k+1) as RealMap of [:T,T:] by A190,FUNCT_2:5,66; A191: abs(fd.p1-fd.q1)>=0 by COMPLEX1:46; A192: fd in Funcs(cT,REAL) by FUNCT_2:8; then A193: Fdistfd.(p1,q1)=abs(fd. p1-fd.q1) by A42; A194: now per cases; suppose k=0; hence Fk1.(p1,q1)>=0 by A42,A183,A190,A192,A191; end; suppose A195: k>0; then Fk1=ADD.(Fk,Nk1) by A184,A189; then A196: Fk1=Fk+Nk1 by A60; Fk.(p1,q1) >= 0 by A187,A188,A195,NAT_1:13; then 0+0<=Fk.(p1,q1)+Nk1.(p1,q1) by A190,A191,A193; hence Fk1.(p1,q1) >=0 by A113,A196,NAGATA_1:def 7; end; end; let Fn be RealMap of [:T,T:]; assume Fn=F.(k+1); hence thesis by A194; end; A197: R[ 0 ]; for n holds R[n] from NAT_1:sch 1(A197,A186); hence thesis by A182,A185; end; end; now A198: AS2.(p1,q1)<=AS1.(p1,q1) by A113,A178,A170,A169,A171,A172,A168, XREAL_1:7; let SumFdist1,SumFdist2 be RealMap of [:T,T:]; assume that A199: SumFdist1=SumFdist.pq1 and A200: SumFdist2 = SumFdist.pq2; SumFdist2=AS2 by A59,A200; hence SumFdist1.pq1 >= SumFdist2.pq1 by A59,A113,A199,A198; end; hence thesis; end; now let p,q,r be Point of T; thus SumFTS.(p,p)=0 proof reconsider pp=[p,p] as Point of [:T,T:] by BORSUK_1:def 2; reconsider SF=SFdist.pp as FinSequence of Fun by FINSEQ_1:def 11; A201: now per cases; suppose A202: len SF=0; A203: ADD is having_a_unity by A60,NAGATA_1:23; then A204: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2; ADD "**" SF=the_unity_wrt ADD by A202,A203,FINSOP_1:def 1; then ADD"**"SF is_a_unity_wrt ADD by A204,BINOP_1:def 8; hence (ADD"**"SF).pp=0 by A111; end; suppose A205: len SF <>0; then len SF >=1 by NAT_1:14; then consider F be Function of NAT,Fun such that A206: F.1 = SF.1 and A207: for n st 0 <> n & n < len SF holds F.(n + 1) = ADD.(F. n,SF.(n + 1 )) and A208: ADD"**"SF = F.(len SF) by FINSOP_1:def 1; defpred R[Element of NAT] means $1<>0 & $1<=len SF implies F.$1. pp=0; A209: for k holds R[k] implies R[k+1] proof let k; assume A210: R[k]; consider x,y be Point of T such that [x,y]=pp and A211: rng SF=RNG(Fx(x)\/Fx(y)) by A57; assume that k+1<>0 and A212: k+1 <=len SF; A213: k< len SF by A212,NAT_1:13; k+1>=1 by NAT_1:14; then k+1 in dom SF by A212,FINSEQ_3:25; then SF.(k+1) in RNG(Fx(x)\/Fx(y)) by A211,FUNCT_1:def 3; then consider fd be RealMap of T such that A214: Fdist.fd =SF.(k+1) and fd in Fx(x)\/Fx(y); fd in Funcs(cT,REAL) by FUNCT_2:8; then reconsider Fdistfd=Fdist.fd,Fk1=F.(k+1),Fk=F.k, SFk1=SF.(k+1) as RealMap of [:T,T:] by A214,FUNCT_2:5,66; fd in Funcs(cT,REAL) by FUNCT_2:8; then A215: Fdistfd.(p,p)=abs(fd.p-fd .p) by A42; per cases; suppose k=0; hence thesis by A206,A214,A215,ABSVALUE:2; end; suppose A216: k>0; then Fk1=ADD.(Fk,SFk1) by A207,A213; then Fk1=Fk+SFk1 by A60; then Fk1.pp=0+SFk1.pp by A210,A212,A216,NAGATA_1:def 7 ,NAT_1:13; hence thesis by A214,A215,ABSVALUE:2; end; end; A217: R[ 0 ]; for n holds R[n] from NAT_1:sch 1(A217,A209); hence (ADD"**"SF).pp=0 by A205,A208; end; end; SumFdist.pp=ADD "**" SF by A59; hence thesis by A201,NAGATA_1:def 8; end; thus SumFTS.(p,r)<=SumFTS.(p,q)+SumFTS.(r,q) 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 Fun by FINSEQ_1:def 11; reconsider ASFpr=ADD"**"SFpr as RealMap of [:T,T:] by FUNCT_2:66; reconsider SumFpr=SumFdist.pr,SumFpq=SumFdist.pq, SumFrq=SumFdist.rq as RealMap of [:T,T:] by FUNCT_2:66; A218: SumFTS.pr = SumFpr.pr & SumFTS.pq = SumFpq.pq by NAGATA_1:def 8; SumFpr.pq <=SumFpq.pq & SumFpr.rq <=SumFrq.rq by A112; then A219: SumFpr.pq + SumFpr.rq <= SumFpq.pq+SumFrq.rq by XREAL_1:7; A220: now per cases; suppose A221: len SFpr = 0; A222: ADD is having_a_unity by A60,NAGATA_1:23; then A223: ex f being Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2; ADD"**"SFpr=the_unity_wrt ADD by A221,A222,FINSOP_1:def 1; then A224: ADD"**"SFpr is_a_unity_wrt ADD by A223,BINOP_1:def 8; then ASFpr.pr=0 & ASFpr.pq=0 by A111; hence ASFpr.pr <= ASFpr.pq + ASFpr.rq by A111,A224; end; suppose A225: len SFpr <> 0; then len SFpr >=1 by NAT_1:14; then consider F be Function of NAT,Fun such that A226: F.1 = SFpr.1 and A227: for n st 0 <> n & n < len SFpr holds F.(n+1)=ADD.(F.n, SFpr.(n+1)) and A228: ADD"**"SFpr=F.(len SFpr) by FINSOP_1:def 1; defpred T[Element of NAT] means $1<>0 & $1<=len SFpr implies for F9 be RealMap of [:T,T:] st F9=F.$1 holds F9.pr<=F9.pq+F9.rq; A229: for k holds T[k] implies T[k+1] proof let k; assume A230: T[k]; consider x,y be Point of T such that [x,y]=pr and A231: rng SFpr=RNG(Fx(x)\/Fx(y)) by A57; assume that k+1<>0 and A232: k+1 <=len SFpr; A233: k=1 by NAT_1:14; then k+1 in dom SFpr by A232,FINSEQ_3:25; then SFpr.(k+1) in RNG(Fx(x)\/Fx(y)) by A231,FUNCT_1:def 3; then consider fd be RealMap of T such that A234: Fdist.fd =SFpr.(k+1) and fd in Fx(x)\/Fx(y); fd in Funcs(cT,REAL) by FUNCT_2:8; then reconsider Fdistfd=Fdist.fd, Fk1=F.(k+1), Fk=F.k, SFk1=SFpr.(k +1) as RealMap of [:T,T:] by A234,FUNCT_2:5,66; A235: fd.p-fd.r=(fd.p-fd.q)+(fd.q-fd.r); then A236: abs(fd.p-fd.r)<=abs(fd.p-fd.q)+ abs(fd.q- fd.r) by COMPLEX1:56 ; A237: fd in Funcs(cT,REAL) by FUNCT_2:8; then A238: Fdistfd.(p,r)= abs(fd.p-fd.r) & Fdistfd.(p,q)=abs(fd.p- fd.q) by A42; A239: abs(fd.q-fd.r)=abs(-(fd.q-fd.r)) & Fdistfd.(r,q)=abs(fd. r-fd.q) by A42,A237,COMPLEX1:52; let F9 be RealMap of [:T,T:] such that A240: F9=F.(k+1); per cases; suppose k=0; hence thesis by A226,A234,A235,A238,A239,A240,COMPLEX1:56; end; suppose A241: k>0; then Fk.pr<=Fk.pq+Fk.rq by A230,A232,NAT_1:13; then A242: Fk.pr+SFk1.pr<=(Fk.pq+Fk.rq)+(SFk1.pq+SFk1.rq) by A234,A236 ,A238,A239,XREAL_1:7; Fk1=ADD.(Fk,SFk1) by A227,A233,A241; then A243: Fk1=Fk+SFk1 by A60; then Fk1.pq=Fk.pq+SFk1.pq & Fk1.rq=Fk.rq+SFk1.rq by NAGATA_1:def 7; hence thesis by A240,A243,A242,NAGATA_1:def 7; end; end; A244: T[ 0 ]; for n holds T[n] from NAT_1:sch 1(A244,A229); hence ASFpr.pr <= ASFpr.pq + ASFpr.rq by A225,A228; end; end; SumFpr=ADD "**" SFpr by A59; then SumFpr.pr<=SumFpq.pq+SumFrq.rq by A220,A219,XXREAL_0:2; hence thesis by A218,NAGATA_1:def 8; end; end; then A245: SumFTS is_a_pseudometric_of cT by NAGATA_1:28; A246: for p be Point of T,fd be Element of Funcs(cT, REAL) st fd in Fx(p) holds funcdist[fd,Fdist.fd] & Fdist.fd is continuous RealMap of [:T,T:] proof let p be Point of T,fd be Element of Funcs(cT,REAL); reconsider FD=Fdist.fd as RealMap of [:T,T:] by FUNCT_2:66; assume fd in Fx(p); then consider A be Subset of T such that A247: fd=Fn.A and A248: A in Bn.n and A in s(Sx.p); A249: funcdist[fd,Fdist.fd] by A42; F[A,Fn.A] by A24,A248; then FD is continuous by A247,A249,NAGATA_1:21; hence thesis by A42; end; A250: for pq9 holds SumFdist.pq9 is continuous RealMap of [:T,T:] proof let pq9; reconsider SF=SFdist.pq9 as FinSequence of Fun by FINSEQ_1:def 11; consider p,q such that [p,q]=pq9 and A251: rng SF=RNG(Fx(p)\/Fx(q)) by A57; for n st 0<>n & n<=len SF holds SF.n is continuous RealMap of [:T ,T:] proof let n; assume that A252: 0<>n and A253: n<=len SF; n>=1 by A252,NAT_1:14; then n in dom SF by A253,FINSEQ_3:25; then SF.n in RNG(Fx(p)\/Fx(q)) by A251,FUNCT_1:def 3; then consider fd be RealMap of T such that A254: SF.n=Fdist.fd and A255: fd in (Fx(p)\/Fx(q)); A256: fd in Funcs(cT,REAL) by FUNCT_2:8; fd in Fx(p) or fd in Fx(q) by A255,XBOOLE_0:def 3; hence thesis by A246,A254,A256; end; then ADD"**"SF is continuous RealMap of [:T,T:] by A60,NAGATA_1:25; hence thesis by A59; end; A257: for pq9 holds SumFdist9.pq9 is continuous Function of [:T,T:],R^1 proof let pq9; reconsider SF=SumFdist.pq9 as Function of [:T,T:],R^1 by A250, TOPMETR:17; SumFdist.pq9 is continuous RealMap of [:T,T:] by A250; then SF is continuous by JORDAN5A:27; hence thesis; end; take min(1,SumFTS9); A258: for p,q holds min(1,SumFTS9).[p,q]<=1 proof let p,q; cTT=[:cT,cT:] by BORSUK_1:def 2; then min(1,SumFTS9).[p,q]=min(1,SumFTS9.[p,q]) by NAGATA_1:def 9; hence thesis by XXREAL_0:17; end; for p,q be Point of [:T,T:] st p in SS.q holds SumFdist9.p.p= SumFdist9.q.p by A112; then SumFdist9 Toler is continuous by A257,A32,NAGATA_1:26; then SumFTS9 is continuous by JORDAN5A:27; then min(1,SumFTS9)=min(1,SumFTS) & min(1,SumFTS9) is continuous by BORSUK_1:def 2,NAGATA_1:27; hence thesis by A245,A258,A109,NAGATA_1:30; end; A259: for k be set st k in NAT ex f be set st f in Funcs(cTT,REAL) & N[k,f ] proof A260: NAT =rng PairFunc by Th2,FUNCT_2:def 3; let k be set; assume k in NAT; then consider nm be set such that A261: nm in dom PairFunc and A262: k=PairFunc.nm by A260,FUNCT_1:def 3; consider n,m be set such that A263: n in NAT & m in NAT and A264: nm=[n,m] by A261,ZFMISC_1:def 2; consider pmet9 such that A265: NN[n,m,pmet9] by A7,A263; take pmet9; thus pmet9 in Funcs(cTT,REAL) by FUNCT_2:8; take pm = pmet9; thus pm = pmet9; let n1,m1 be Element of NAT; assume PairFunc".k=[n1,m1]; then [n1,m1]=[n,m] by A261,A262,A264,Lm2,Th2,FUNCT_1:32; then n1=n & m1=m by XTUPLE_0:1; hence thesis by A265; end; consider F be Function of NAT,Funcs(cTT,REAL) such that A266: for n be set st n in NAT holds N[n,F.n] from FUNCT_2:sch 1(A259); A267: now let n; [:cT,cT:]=cTT by BORSUK_1:def 2; hence F.n is PartFunc of [:cT,cT:],REAL by FUNCT_2:66; end; dom F=NAT by FUNCT_2:def 1; then reconsider F9=F as Functional_Sequence of[:cT,cT:],REAL by A267, SEQFUNC:1; A268: for p,A9 st not p in A9 & A9 is closed ex k st for pmet st F9.k=pmet holds lower_bound(pmet,A9).p>0 proof let p,A9 such that A269: not p in A9 and A270: A9 is closed; set O=A9`; p in O by A269,XBOOLE_0:def 5; then consider U be Subset of T such that A271: p in U and A272: Cl U c=O and A273: U in Union Bn by A1,A5,A270,NAGATA_1:19; Union Bn c=the topology of T by A5,TOPS_2:64; then reconsider U as open Subset of T by A273,PRE_TOPC:def 2; consider n such that A274: U in Bn.n by A273,PROB_1:12; consider W be Subset of T such that A275: p in W & Cl W c=U and A276: W in Union Bn by A1,A5,A271,NAGATA_1:19; Union Bn c=the topology of T by A5,TOPS_2:64; then reconsider W as open Subset of T by A276,PRE_TOPC:def 2; consider m such that A277: W in Bn.m by A276,PROB_1:12; set k=PairFunc.[n,m]; consider G be RealMap of [:T,T:] such that A278: G = F.k and A279: for n,m st PairFunc".k=[n,m] holds NN[n,m,G] by A266; dom PairFunc = [:NAT,NAT:] by FUNCT_2:def 1; then [n,m]=PairFunc".k by Lm2,Th2,FUNCT_1:32; then consider pmet such that A280: G=pmet and G is continuous and pmet is_a_pseudometric_of cT and A281: for p,q holds pmet.[p,q]<=1 & for p,q st ex A,B st A is open & B is open & A in Bn.m & B in Bn.n & p in A & Cl A c= B & not q in B holds pmet. [p,q] = 1 by A279; A282: for rn st rn in (dist(pmet,p)).:A9 holds rn>=1 proof let rn; assume rn in (dist(pmet,p)).:A9; then consider a be set such that A283: a in dom dist(pmet,p) and A284: a in A9 and A285: rn=(dist(pmet,p)).a by FUNCT_1:def 6; reconsider a as Point of T by A283; A286: pmet.(p,a)=dist(pmet,p).a by Def2; U c= Cl U by PRE_TOPC:18; then U c= O by A272,XBOOLE_1:1; then U misses A9 by SUBSET_1:23; then not a in U by A284,XBOOLE_0:3; hence thesis by A275,A274,A277,A281,A285,A286; end; take k; cT=dom dist(pmet,p) by FUNCT_2:def 1; then lower_bound ((dist(pmet,p)).:A9) >= 1 by A282,SEQ_4:43; hence thesis by A278,A280,Def3; end; for k ex pmet st F9.k=pmet & pmet is_a_pseudometric_of cT & (for pq holds pmet.pq<=1) & for pmet9 st pmet=pmet9 holds pmet9 is continuous proof let k; consider Fk be RealMap of [:T,T:] such that A287: Fk = F.k and A288: for n,m st PairFunc".k=[n,m] holds NN[n,m,Fk] by A266; NAT =rng PairFunc by Th2,FUNCT_2:def 3; then consider nm be set such that A289: nm in dom PairFunc and A290: k=PairFunc.nm by FUNCT_1:def 3; consider n,m be set such that A291: n in NAT & m in NAT and A292: nm=[n,m] by A289,ZFMISC_1:def 2; [n,m]=PairFunc".k by A289,A290,A292,Lm2,Th2,FUNCT_1:32; then consider pmet such that A293: Fk=pmet and A294: Fk is continuous and A295: pmet is_a_pseudometric_of cT and A296: for p,q holds pmet.[p,q]<=1 & for p,q st ex A,B st A is open & B is open & A in Bn.m & B in Bn.n & p in A & Cl A c= B & not q in B holds pmet. [p,q] = 1 by A291,A288; take pmet; thus F9.k=pmet & pmet is_a_pseudometric_of cT by A287,A293,A295; thus for pq holds pmet.pq<=1 proof let pq; ex p,q be set st p in cT & q in cT & pq=[p,q] by ZFMISC_1:def 2; hence thesis by A296; end; thus thesis by A293,A294; end; hence thesis by A2,A268,Th17; end; thus thesis by NAGATA_1:15,16; end; theorem Th20: T is metrizable implies for FX be Subset-Family of T st FX is Cover of T & FX is open ex Un be FamilySequence of T st Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete proof set cT=the carrier of T; assume T is metrizable; then consider metr be Function of [:cT,cT:],REAL such that A1: metr is_metric_of cT and A2: Family_open_set(SpaceMetr(cT,metr))=the topology of T by PCOMPS_1:def 8; reconsider PM=SpaceMetr(cT,metr) as non empty MetrSpace by A1,PCOMPS_1:36; set cPM= the carrier of PM; let FX be Subset-Family of T such that A3: FX is Cover of T and A4: FX is open; defpred P1[set] means $1 in FX; deffunc F1(Point of PM,Nat)=Ball($1,1/(2|^($2+1))); consider R be Relation such that A5: R well_orders FX by WELLORD2:17; consider Mn be Relation such that A6: Mn = R |_2 FX; set UB ={union {Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) & Ball(c,3/2) c= V} where V is Subset of PM:V in FX}; UB c= bool the carrier of PM proof let x; assume x in UB; then consider V be Subset of PM such that A7: x=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn ) & Ball(c,3/2)c= V} and V in FX; x c= cPM proof let y; assume y in x; then consider W be set such that A8: y in W and A9: W in {Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn )& Ball(c,3/2)c=V} by A7,TARSKI:def 4; ex c be Point of PM st W=Ball(c,1/2) & c in V\PartUnion(V,Mn)& Ball (c,3/2) c= V by A9; hence thesis by A8; end; hence thesis; end; then reconsider UB as Subset-Family of PM; defpred Q1[Point of PM,Subset of PM,Nat] means $1 in $2\PartUnion($2,Mn) & Ball($1,3/(2|^($3+1)))c= $2; consider Un be Function of NAT,bool bool cPM such that A10: Un.0 = UB & for n holds Un.(n+1)= {union{F1(c,n) where c is Point of PM:Q1[c,V,n] & not c in union{union (Un.k): k <= n}} where V is Subset of PM : P1[V]} from PCOMPS_2:sch 3; reconsider Un9=Un as FamilySequence of T by A1,PCOMPS_2:4; take Un9; thus Union Un9 is open proof let A; assume A in Union Un9; then consider n such that A11: A in Un.n by PROB_1:12; per cases; suppose n=0; then consider V be Subset of PM such that A12: A=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V, Mn) & Ball(c,3/2) c= V} and V in FX by A10,A11; set BALL={Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) & Ball(c,3/2) c= V}; BALL c= bool the carrier of PM proof let x; assume x in BALL; then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn )& Ball(c,3/2) c= V; hence thesis; end; then reconsider BALL as Subset-Family of PM; BALL c= Family_open_set PM proof let x; assume x in BALL; then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn )& Ball(c,3/2) c= V; hence thesis by PCOMPS_1:29; end; then A in the topology of T by A2,A12,PCOMPS_1:32; hence thesis by PRE_TOPC:def 2; end; suppose n>0; then consider m being Nat such that A13: n=m+1 by NAT_1:6; reconsider m as Element of NAT by ORDINAL1:def 12; A in {union{F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in union{union (Un.k): k <= m}} where V is Subset of PM: P1[V]} by A10,A11,A13; then consider V be Subset of PM such that A14: A=union{F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in union{union (Un.k): k <= m}} & P1[V]; set BALL={F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in union{union (Un.k): k <= m}}; BALL c= bool the carrier of PM proof let x; assume x in BALL; then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{ union (Un.k): k <= m}; hence thesis; end; then reconsider BALL as Subset-Family of PM; BALL c= Family_open_set PM proof let x; assume x in BALL; then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{ union (Un.k): k <= m}; hence thesis by PCOMPS_1:29; end; then A in the topology of T by A2,A14,PCOMPS_1:32; hence thesis by PRE_TOPC:def 2; end; end; A15: Mn well_orders FX by A5,A6,PCOMPS_2:1; [#]T c= union Union Un9 proof let x such that A16: x in [#]T; reconsider x9=x as Element of PM by A1,A16,PCOMPS_2:4; defpred P2[set] means x in $1; ex G be Subset of T st x in G & G in FX by A3,A16,PCOMPS_1:3; then A17: ex G be set st G in FX & P2[G]; consider X such that A18: X in FX & P2[X] & for Y be set st Y in FX & P2[Y] holds [X,Y] in Mn from PCOMPS_2:sch 1(A15,A17); assume A19: not x in union Union Un9; A20: for V be set,n be Element of NAT st V in Un9.n holds not x in V proof let V be set,n be Element of NAT; assume V in Un9.n; then V in Union Un by PROB_1:12; hence thesis by A19,TARSKI:def 4; end; A21: for n holds not x in union (Un9.n) proof let n; assume x in union (Un9.n); then ex V be set st x in V & V in Un9.n by TARSKI:def 4; hence contradiction by A20; end; reconsider X as Subset of T by A18; X is open by A4,A18,TOPS_2:def 1; then A22: X in Family_open_set PM by A2,PRE_TOPC:def 2; reconsider X as Subset of PM by A1,PCOMPS_2:4; consider r such that A23: r>0 and A24: Ball(x9,r) c= X by A18,A22,PCOMPS_1:def 4; defpred P3[Nat] means 3/(2 |^ $1) <= r; ex k st P3[k] by A23,PREPOWER:92; then A25: ex k be Nat st P3[k]; consider k be Nat such that A26: P3[k] & for i be Nat st P3[i] holds k <= i from NAT_1:sch 5(A25); set W=union{F1(y,k) where y is Point of PM:Q1[y,X,k] & not y in union{ union(Un.i):i <= k}}; 2|^(k+1)=2|^k*2 by NEWTON:6; then 2|^k > 0 & 2|^(k+1) >= 2|^k by PREPOWER:6,XREAL_1:151; then 3/2 |^(k+1) <= 3/2|^k by XREAL_1:118; then A27: 3/2 |^(k+1) <= r by A26,XXREAL_0:2; A28: x in W proof not x9 in PartUnion(X,Mn) proof assume x9 in PartUnion(X,Mn); then x9 in union (Mn-Seg(X)) by PCOMPS_2:def 1; then consider M be set such that A29: x9 in M and A30: M in Mn-Seg(X) by TARSKI:def 4; A31: M <> X by A30,WELLORD1:1; A32: Mn is_antisymmetric_in FX by A15,WELLORD1:def 5; A33: [M,X] in Mn by A30,WELLORD1:1; then M in field Mn by RELAT_1:15; then A34: M in FX by A5,A6,PCOMPS_2:1; then [X,M] in Mn by A18,A29; hence contradiction by A18,A31,A33,A34,A32,RELAT_2:def 4; end; then A35: x9 in X\PartUnion(X,Mn) by A18,XBOOLE_0:def 5; set A=Ball(x9,1/(2|^(k+1))); 0 < 2|^(k+1) by PREPOWER:6; then A36: x9 in A by TBSP_1:11,XREAL_1:139; A37: not x9 in union{union(Un9.i):i <= k} proof assume x9 in union {union(Un9.i):i <= k}; then consider D be set such that A38: x9 in D & D in {union(Un9.i):i <= k} by TARSKI:def 4; ex i st D=union (Un9.i) & i <= k by A38; hence contradiction by A21,A38; end; Ball(x9,3/(2|^(k+1))) c= Ball(x9,r) by A27,PCOMPS_1:1; then Ball(x9,3/(2|^(k+1))) c= X by A24,XBOOLE_1:1; then A in {F1(y,k) where y is Point of PM:Q1[y,X,k] & not y in union { union(Un9.i): i <= k}} by A35,A37; hence thesis by A36,TARSKI:def 4; end; k in NAT & W in {union{F1(y,k)where y is Point of PM: Q1[y,V,k] & not y in union {union(Un.q) where q is Element of NAT: q <= k}} where V is Subset of PM: V in FX} by A18,ORDINAL1:def 12; then W in Un9.(k+1) by A10; hence thesis by A20,A28; end; then [#]T = union Union Un9 by XBOOLE_0:def 10; hence Union Un9 is Cover of T by SETFAM_1:45; for X be set st X in Union Un9 ex Y be set st Y in FX & X c= Y proof let X be set; assume X in Union Un9; then consider n such that A39: X in Un.n by PROB_1:12; per cases; suppose n=0; then consider V be Subset of PM such that A40: X=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V, Mn) & Ball(c,3/2) c= V} and A41: V in FX by A10,A39; set BALL={Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) & Ball(c,3/2) c= V}; BALL c= bool the carrier of PM proof let x; assume x in BALL; then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn) & Ball(c,3/2) c= V; hence thesis; end; then reconsider BALL as Subset-Family of PM; for W be set st W in BALL holds W c= V proof let W be set; assume W in BALL; then consider c be Element of PM such that A42: W=Ball(c,1/2) and c in V\PartUnion(V,Mn) and A43: Ball(c,3/2) c= V; Ball(c,1/2) c= Ball(c,3/2) by PCOMPS_1:1; hence thesis by A42,A43,XBOOLE_1:1; end; then X c= V by A40,ZFMISC_1:76; hence thesis by A41; end; suppose n>0; then consider m being Nat such that A44: n=m+1 by NAT_1:6; reconsider m as Element of NAT by ORDINAL1:def 12; X in {union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in union{union (Un.k): k <= m}} where V is Subset of PM: P1[V]} by A10,A39,A44; then consider V be Subset of PM such that A45: X=union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in union{union (Un.k): k <= m}} & P1[V]; set BALL={F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in union{ union (Un.k): k <= m}}; BALL c= bool the carrier of PM proof let x; assume x in BALL; then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{ union (Un.k): k <= m}; hence thesis; end; then reconsider BALL as Subset-Family of PM; for W be set st W in BALL holds W c= V proof let W be set; assume W in BALL; then consider c be Element of PM such that A46: W=F1(c,m) & Q1[c,V,m] & not c in union{union (Un.k): k <= m}; 0 < 2|^(m+1) by PREPOWER:6; then 1/(2|^(m+1)) < 3/(2|^(m+1)) by XREAL_1:74; then F1(c,m)c=Ball(c,3/(2|^(m+1))) by PCOMPS_1:1; hence thesis by A46,XBOOLE_1:1; end; then X c= V by A45,ZFMISC_1:76; hence thesis by A45; end; end; hence Union Un9 is_finer_than FX by SETFAM_1:def 2; for n holds Un9.n is discrete proof let n; for p ex O be open Subset of T st p in O & for A,B st A in Un9.n & B in Un9.n holds O meets A & O meets B implies A=B proof let p; reconsider p9=p as Point of PM by A1,PCOMPS_2:4; set O=Ball(p9,1/(2|^(n+2))); O in Family_open_set PM by PCOMPS_1:29; then reconsider O as open Subset of T by A2,PRE_TOPC:def 2; take O; A47: now let A,B such that A48: A in Un9.n and A49: B in Un9.n; assume that A50: O meets A and A51: O meets B; consider a be set such that A52: a in O and A53: a in A by A50,XBOOLE_0:3; consider b be set such that A54: b in O and A55: b in B by A51,XBOOLE_0:3; reconsider a,b as Point of PM by A52,A54; A56: dist(p9,b)<1/(2|^(n+2)) by A54,METRIC_1:11; A57: dist(a,b)<=dist(a,p9)+dist(p9,b) & 2|^(n+1+1)=2|^(n+1)*2 by METRIC_1:4 ,NEWTON:6; dist(p9,a)<1/(2|^(n+2)) by A52,METRIC_1:11; then dist(a,p9)+dist(p9,b)<1/(2|^(n+2))+1/(2|^(n+2)) by A56,XREAL_1:8; then dist(a,b)<2*(1/(2*2|^(n+1))) by A57,XXREAL_0:2; then dist(a,b)<(2*1) /(2*2|^(n+1)) by XCMPLX_1:74; then A58: dist(a,b)<(2/2*1)/2|^(n+1) by XCMPLX_1:83; now per cases; suppose A59: n=0; then A60: dist(a,b)<1/2 by A58,NEWTON:5; consider V be Subset of PM such that A61: A=union {Ball(c,1/2) where c is Point of PM: c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V} and A62: V in FX by A10,A48,A59; consider Ba be set such that A63: a in Ba and A64: Ba in {Ball(c,1/2) where c is Point of PM: c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V} by A53,A61,TARSKI:def 4; consider ca be Point of PM such that A65: Ba=Ball(ca,1/2) and A66: ca in V\PartUnion(V,Mn) and A67: Ball(ca,3/2) c= V by A64; dist(ca,a)<1/2 by A63,A65,METRIC_1:11; then A68: dist(ca,a)+dist(a,b)<1/2+1/2 by A60,XREAL_1:8; dist(ca,b)<=dist(ca,a)+ dist(a,b) by METRIC_1:4; then A69: dist(ca,b)<1 by A68,XXREAL_0:2; consider W be Subset of PM such that A70: B=union {Ball(c,1/2) where c is Point of PM: c in W\ PartUnion(W,Mn) & Ball(c,3/2) c= W} and A71: W in FX by A10,A49,A59; consider Bb be set such that A72: b in Bb and A73: Bb in {Ball(c,1/2) where c is Point of PM: c in W\ PartUnion(W,Mn) & Ball(c,3/2) c= W} by A55,A70,TARSKI:def 4; consider cb be Point of PM such that A74: Bb=Ball(cb,1/2) and A75: cb in W\PartUnion(W,Mn) and A76: Ball(cb,3/2) c= W by A73; A77: dist(ca,cb)<=dist(ca,b)+ dist(b,cb) by METRIC_1:4; dist(cb,b)<1/2 by A72,A74,METRIC_1:11; then dist(ca,b)+dist(b,cb)<1+1/2 by A69,XREAL_1:8; then dist(ca,cb)<3/2 by A77,XXREAL_0:2; then A78: ca in Ball(cb,3/2) & cb in Ball(ca,3/2) by METRIC_1:11; V=W proof assume A79: V<>W; Mn is_connected_in FX by A15,WELLORD1:def 5; then [V,W] in Mn or [W,V] in Mn by A62,A71,A79,RELAT_2:def 6; then V in Mn-Seg(W) or W in Mn-Seg(V)by A79,WELLORD1:1; then cb in union(Mn-Seg(W)) or ca in union(Mn-Seg(V)) by A67,A76 ,A78,TARSKI:def 4; then cb in PartUnion(W,Mn) or ca in PartUnion(V,Mn) by PCOMPS_2:def 1; hence thesis by A66,A75,XBOOLE_0:def 5; end; hence A=B by A61,A70; end; suppose n>0; then consider m being Nat such that A80: n=m+1 by NAT_1:6; set r=1/(2|^n); A81: 3*r=(3*1)/2|^n by XCMPLX_1:74; 2|^(n+1)=2|^n*2 by NEWTON:6; then 2|^n>0 & 2|^(n+1)>=2|^n by PREPOWER:6,XREAL_1:151; then 1/2|^(n+1) <= r by XREAL_1:118; then A82: dist(a,b)W; Mn is_connected_in FX by A15,WELLORD1:def 5; then [V,W] in Mn or [W,V] in Mn by A83,A88,A93,RELAT_2:def 6; then V in Mn-Seg(W) or W in Mn-Seg(V)by A93,WELLORD1:1; then cb in union(Mn-Seg(W)) or ca in union(Mn-Seg(V)) by A85,A90 ,A92,TARSKI:def 4; then cb in PartUnion(W,Mn) or ca in PartUnion(V,Mn) by PCOMPS_2:def 1; hence thesis by A85,A90,XBOOLE_0:def 5; end; hence A=B by A83,A88; end; end; hence A=B; end; 0 < 2|^(n+2) by PREPOWER:6; hence thesis by A47,TBSP_1:11,XREAL_1:139; end; hence thesis by NAGATA_1:def 1; end; hence Un9 is sigma_discrete by NAGATA_1:def 2; end; theorem Th21: for T st T is metrizable ex Un be FamilySequence of T st Un is Basis_sigma_discrete proof let T such that A1: T is metrizable; consider metr be Function of [:the carrier of T,the carrier of T:],REAL such that A2: metr is_metric_of the carrier of T and A3: Family_open_set(SpaceMetr (the carrier of T,metr)) = the topology of T by A1,PCOMPS_1:def 8; set bbcT=bool bool the carrier of T; reconsider PM = SpaceMetr(the carrier of T,metr) as non empty MetrSpace by A2 ,PCOMPS_1:36; deffunc BALL(set)={Ball(x, 1/(2 |^ (In($1,NAT)))) where x is Point of PM: x is Point of PM}; A4: for k be set st k in NAT holds BALL(k) in bool bool the carrier of T proof let k be set; assume k in NAT; then reconsider k as Element of NAT; BALL(k) c= bool the carrier of T proof A5: In(k,NAT) = k by FUNCT_7:def 1; let B be set; assume B in BALL(k); then ex x be Point of PM st B=Ball(x,1/(2|^k)) & x is Point of PM by A5; then B in Family_open_set PM by PCOMPS_1:29; hence thesis by A3; end; hence thesis; end; consider FB be FamilySequence of T such that A6: for k be set st k in NAT holds FB.k= BALL(k) from FUNCT_2:sch 2(A4); defpred U[set,set] means ex FS be FamilySequence of T st $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB.$1 & FS is sigma_discrete; set TPM = TopSpaceMetr PM; A7: TPM = TopStruct (#the carrier of PM,Family_open_set PM#) by PCOMPS_1:def 5; then A8: [#]T=[#]TPM by A2,PCOMPS_2:4; A9: for n be Element of NAT ex Un be Element of Funcs(NAT,bbcT) st U[n,Un] proof let n be Element of NAT; A10: n = In(n,NAT) by FUNCT_7:def 1; now let U be Subset of T; assume U in (FB.n); then U in BALL(n) by A6; then ex x be Point of PM st U = Ball(x,1/(2|^ n)) & x is Point of PM by A10; then U in the topology of T by A3,PCOMPS_1:29; hence U is open by PRE_TOPC:def 2; end; then A11: FB.n is open by TOPS_2:def 1; A12: [#]TPM c= union (FB.n) proof let x; assume x in [#]TPM; then reconsider x9=x as Element of PM by A7; 2|^n > 0 by NEWTON:83; then A13: x9 in Ball(x9,1/(2|^ n)) by TBSP_1:11,XREAL_1:139; Ball(x9,1/(2|^ n)) in BALL(n) by A10; then Ball(x9,1/(2|^ n)) in FB.n by A6; hence thesis by A13,TARSKI:def 4; end; union (FB.n) c= [#]TPM proof given x such that A14: x in union (FB.n) and A15: not x in [#]TPM; consider A be set such that A16: x in A and A17: A in (FB.n) by A14,TARSKI:def 4; A in BALL(n) by A6,A17; then ex y be Point of PM st A=Ball(y,1/(2|^n)) & y is Point of PM by A10; hence thesis by A7,A15,A16; end; then [#]TPM = union (FB.n) by A12,XBOOLE_0:def 10; then (FB.n) is Cover of T by A8,SETFAM_1:45; then consider Un be FamilySequence of T such that A18: Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB. n & Un is sigma_discrete by A1,A11,Th20; Un in Funcs(NAT,bbcT) by FUNCT_2:8; hence thesis by A18; end; consider Un be Function of NAT,Funcs(NAT,bbcT) such that A19: for n be Element of NAT holds U[n,Un.n] from FUNCT_2:sch 3(A9); defpred X[set,set] means for n,m st PairFunc.[n,m]=$1 for Unn be FamilySequence of T st Unn=Un.n holds $2=Unn.m; A20: for k be set st k in NAT ex Ux be set st Ux in bbcT & X[k,Ux] proof let k be set; assume k in NAT; then reconsider k9=k as Element of NAT; NAT =rng PairFunc by Th2,FUNCT_2:def 3; then consider nm be set such that A21: nm in dom PairFunc and A22: k9=PairFunc.nm by FUNCT_1:def 3; consider n,m be set such that A23: n in NAT and A24: m in NAT and A25: nm=[n,m] by A21,ZFMISC_1:def 2; reconsider Unn=Un.n as FamilySequence of T by A23,FUNCT_2:5,66; take Ux=Unn.m; dom Unn = NAT by PARTFUN1:def 2; then m in dom Unn by A24; then Ux in rng Unn by FUNCT_1:3; hence Ux in bbcT; now let n1,m1 be Element of NAT such that A26: PairFunc.[n1,m1]=k; now let Unn be FamilySequence of T such that A27: Unn=Un.n1; A28: [n,m]=[n1,m1] by A21,A22,A25,A26,Th2,FUNCT_2:19; then n1=n by XTUPLE_0:1; hence Ux=Unn.m1 by A27,A28,XTUPLE_0:1; end; hence for Unn be FamilySequence of T st Unn=Un.n1 holds Ux=Unn.m1; end; hence thesis; end; consider UX be Function of NAT,bbcT such that A29: for k be set st k in NAT holds X[k,UX.k] from FUNCT_2:sch 1(A20); A30: for A st A is open for p st p in A ex B st B in Union UX & p in B & B c= A proof let A; assume A is open; then A31: A in Family_open_set PM by A3,PRE_TOPC:def 2; let p such that A32: p in A; reconsider p as Element of PM by A32,A31; consider r such that A33: r>0 and A34: Ball(p,r) c=A by A32,A31,PCOMPS_1:def 4; consider n such that A35: 1/(2|^n)<=r by A33,PREPOWER:92; consider Unn1 be FamilySequence of T such that A36: Un.(n+1) = Unn1 and Union Unn1 is open and A37: Union Unn1 is Cover of T and A38: Union Unn1 is_finer_than FB.(n+1) and Unn1 is sigma_discrete by A19; union (Union Unn1) = [#]T by A37,SETFAM_1:45; then consider B be set such that A39: p in B and A40: B in (Union Unn1) by TARSKI:def 4; reconsider B as Subset of PM by A2,A40,PCOMPS_2:4; consider B1 be set such that A41: B1 in FB.(n+1) and A42: B c= B1 by A38,A40,SETFAM_1:def 2; consider k such that A43: B in Unn1.k by A40,PROB_1:12; n + 1 = In(n+1,NAT) & B1 in BALL(n+1) by A6,A41,FUNCT_7:def 1; then consider q be Point of PM such that A44: B1=Ball(q,(1/(2|^(n+1)))) and q is Element of PM; now let s be Element of PM; assume s in B; then A45: dist(q,s)<1/(2|^(n+1)) by A42,A44,METRIC_1:11; dist(q,p)<1/(2|^(n+1)) by A39,A42,A44,METRIC_1:11; then dist(p,s)<=dist(q,p)+dist(q,s) & dist(q,p)+dist(q,s)<1/(2|^(n+1))+ 1/(2|^(n+1 )) by A45,METRIC_1:4,XREAL_1:8; then dist(p,s)<2*(1/(2|^(n+1))) by XXREAL_0:2; then dist(p,s)<(1/(2|^n * 2))*2 by NEWTON:6; then dist(p,s)<(1/(2|^n)) by XCMPLX_1:92; then dist(p,s)