:: FRECHET2 semantic presentation begin Lm1: for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds T is T_1 proof let T be non empty TopSpace; ::_thesis: ( ( for p being Point of T holds Cl {p} = {p} ) implies T is T_1 ) assume A1: for p being Point of T holds Cl {p} = {p} ; ::_thesis: T is T_1 for p being Point of T holds {p} is closed proof let p be Point of T; ::_thesis: {p} is closed Cl {p} = {p} by A1; hence {p} is closed by PRE_TOPC:22; ::_thesis: verum end; hence T is T_1 by URYSOHN1:19; ::_thesis: verum end; Lm2: for T being non empty TopSpace st not T is T_1 holds ex x1, x2 being Point of T st ( x1 <> x2 & x2 in Cl {x1} ) proof let T be non empty TopSpace; ::_thesis: ( not T is T_1 implies ex x1, x2 being Point of T st ( x1 <> x2 & x2 in Cl {x1} ) ) assume not T is T_1 ; ::_thesis: ex x1, x2 being Point of T st ( x1 <> x2 & x2 in Cl {x1} ) then consider x1 being Point of T such that A1: Cl {x1} <> {x1} by Lm1; ( not {x1} c= Cl {x1} or not Cl {x1} c= {x1} ) by A1, XBOOLE_0:def_10; then consider x2 being set such that A2: x2 in Cl {x1} and A3: not x2 in {x1} by PRE_TOPC:18, TARSKI:def_3; reconsider x2 = x2 as Point of T by A2; take x1 ; ::_thesis: ex x2 being Point of T st ( x1 <> x2 & x2 in Cl {x1} ) take x2 ; ::_thesis: ( x1 <> x2 & x2 in Cl {x1} ) thus x1 <> x2 by A3, TARSKI:def_1; ::_thesis: x2 in Cl {x1} thus x2 in Cl {x1} by A2; ::_thesis: verum end; Lm3: for T being non empty TopSpace st not T is T_1 holds ex x1, x2 being Point of T ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) proof let T be non empty TopSpace; ::_thesis: ( not T is T_1 implies ex x1, x2 being Point of T ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) ) assume not T is T_1 ; ::_thesis: ex x1, x2 being Point of T ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) then consider x1, x2 being Point of T such that A1: x1 <> x2 and A2: x2 in Cl {x1} by Lm2; set S = NAT --> x1; take x1 ; ::_thesis: ex x2 being Point of T ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) take x2 ; ::_thesis: ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) take NAT --> x1 ; ::_thesis: ( NAT --> x1 = NAT --> x1 & x1 <> x2 & NAT --> x1 is_convergent_to x2 ) thus NAT --> x1 = NAT --> x1 ; ::_thesis: ( x1 <> x2 & NAT --> x1 is_convergent_to x2 ) thus x1 <> x2 by A1; ::_thesis: NAT --> x1 is_convergent_to x2 thus NAT --> x1 is_convergent_to x2 ::_thesis: verum proof let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x2 in U1 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or (NAT --> x1) . b2 in U1 ) ) assume A3: ( U1 is open & x2 in U1 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or (NAT --> x1) . b2 in U1 ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or (NAT --> x1) . b1 in U1 ) {x1} meets U1 by A2, A3, PRE_TOPC:def_7; then x1 in U1 by ZFMISC_1:50; hence for b1 being Element of NAT holds ( not 0 <= b1 or (NAT --> x1) . b1 in U1 ) by FUNCOP_1:7; ::_thesis: verum end; end; Lm4: for T being non empty TopSpace st T is T_2 holds T is T_1 proof let T be non empty TopSpace; ::_thesis: ( T is T_2 implies T is T_1 ) assume T is T_2 ; ::_thesis: T is T_1 then for p being Point of T holds {p} is closed by PCOMPS_1:7; hence T is T_1 by URYSOHN1:19; ::_thesis: verum end; theorem :: FRECHET2:1 for T being non empty 1-sorted for S being sequence of T for NS being increasing sequence of NAT holds S * NS is sequence of T ; theorem :: FRECHET2:2 for RS being Real_Sequence st RS = id NAT holds RS is increasing sequence of NAT ; theorem Th3: :: FRECHET2:3 for T being non empty 1-sorted for S being sequence of T for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds not S . m in A proof let T be non empty 1-sorted ; ::_thesis: for S being sequence of T for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds not S . m in A let S be sequence of T; ::_thesis: for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds not S . m in A let A be Subset of T; ::_thesis: ( ( for S1 being subsequence of S holds not rng S1 c= A ) implies ex n being Element of NAT st for m being Element of NAT st n <= m holds not S . m in A ) assume A1: for S1 being subsequence of S holds not rng S1 c= A ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds not S . m in A defpred S1[ set ] means $1 in A; assume for n being Element of NAT ex m being Element of NAT st ( n <= m & S . m in A ) ; ::_thesis: contradiction then A2: for n being Element of NAT ex m being Element of NAT st ( n <= m & S1[S . m] ) ; consider S1 being subsequence of S such that A3: for n being Element of NAT holds S1[S1 . n] from VALUED_1:sch_1(A2); rng S1 c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S1 or y in A ) assume y in rng S1 ; ::_thesis: y in A then consider x1 being set such that A4: x1 in dom S1 and A5: S1 . x1 = y by FUNCT_1:def_3; reconsider n = x1 as Element of NAT by A4; S1 . n in A by A3; hence y in A by A5; ::_thesis: verum end; hence contradiction by A1; ::_thesis: verum end; theorem Th4: :: FRECHET2:4 for T being non empty 1-sorted for S being sequence of T for A, B being Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st ( rng S1 c= A or rng S1 c= B ) proof let T be non empty 1-sorted ; ::_thesis: for S being sequence of T for A, B being Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st ( rng S1 c= A or rng S1 c= B ) let S be sequence of T; ::_thesis: for A, B being Subset of T st rng S c= A \/ B holds ex S1 being subsequence of S st ( rng S1 c= A or rng S1 c= B ) let A, B be Subset of T; ::_thesis: ( rng S c= A \/ B implies ex S1 being subsequence of S st ( rng S1 c= A or rng S1 c= B ) ) assume A1: rng S c= A \/ B ; ::_thesis: ex S1 being subsequence of S st ( rng S1 c= A or rng S1 c= B ) assume A2: for S1 being subsequence of S holds ( not rng S1 c= A & not rng S1 c= B ) ; ::_thesis: contradiction then consider n1 being Element of NAT such that A3: for m being Element of NAT st n1 <= m holds not S . m in A by Th3; consider n2 being Element of NAT such that A4: for m being Element of NAT st n2 <= m holds not S . m in B by A2, Th3; reconsider n = max (n1,n2) as Element of NAT ; A5: not S . n in B by A4, XXREAL_0:25; n in NAT ; then n in dom S by NORMSP_1:12; then A6: S . n in rng S by FUNCT_1:def_3; not S . n in A by A3, XXREAL_0:25; hence contradiction by A1, A5, A6, XBOOLE_0:def_3; ::_thesis: verum end; Lm5: for T being non empty TopSpace st T is first-countable holds for x being Point of T ex B being Basis of x ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) proof let T be non empty TopSpace; ::_thesis: ( T is first-countable implies for x being Point of T ex B being Basis of x ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) ) assume A1: T is first-countable ; ::_thesis: for x being Point of T ex B being Basis of x ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) let x be Point of T; ::_thesis: ex B being Basis of x ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) consider B1 being Basis of x such that A2: B1 is countable by A1, FRECHET:def_2; consider f being Function of NAT,B1 such that A3: rng f = B1 by A2, CARD_3:96; defpred S1[ set , set ] means $2 = meet (f .: (succ $1)); A4: for n being set st n in NAT holds ex A being set st S1[n,A] ; consider S being Function such that A5: dom S = NAT and A6: for n being set st n in NAT holds S1[n,S . n] from CLASSES1:sch_1(A4); A7: rng S c= bool the carrier of T proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in rng S or A in bool the carrier of T ) assume A in rng S ; ::_thesis: A in bool the carrier of T then consider n being set such that A8: ( n in dom S & A = S . n ) by FUNCT_1:def_3; reconsider fsuccn = f .: (succ n) as Subset-Family of T by XBOOLE_1:1; meet fsuccn = meet (f .: (succ n)) ; then meet (f .: (succ n)) in bool the carrier of T ; hence A in bool the carrier of T by A5, A6, A8; ::_thesis: verum end; then reconsider B = rng S as Subset-Family of T ; reconsider B = B as Subset-Family of T ; A9: ex A being set st A in B proof take A = meet (f .: (succ 0)); ::_thesis: A in B A = S . 0 by A6; hence A in B by A5, FUNCT_1:def_3; ::_thesis: verum end; then A10: Intersect B = meet B by SETFAM_1:def_9; for A being set st A in B holds x in A proof let A be set ; ::_thesis: ( A in B implies x in A ) assume A in B ; ::_thesis: x in A then consider n being set such that A11: n in dom S and A12: A = S . n by FUNCT_1:def_3; ( dom f = NAT & n in succ n ) by FUNCT_2:def_1, ORDINAL1:6; then A13: f . n in f .: (succ n) by A5, A11, FUNCT_1:def_6; A14: for A1 being set st A1 in f .: (succ n) holds x in A1 proof let A1 be set ; ::_thesis: ( A1 in f .: (succ n) implies x in A1 ) assume A1 in f .: (succ n) ; ::_thesis: x in A1 then consider m being set such that A15: m in dom f and m in succ n and A16: A1 = f . m by FUNCT_1:def_6; f . m in rng f by A15, FUNCT_1:def_3; then reconsider A2 = A1 as Subset of T by A3, A16; reconsider A2 = A2 as Subset of T ; A2 in B1 by A3, A15, A16, FUNCT_1:def_3; hence x in A1 by YELLOW_8:12; ::_thesis: verum end; A = meet (f .: (succ n)) by A5, A6, A11, A12; hence x in A by A14, A13, SETFAM_1:def_1; ::_thesis: verum end; then A17: x in meet B by A9, SETFAM_1:def_1; A18: B c= the topology of T proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in B or A in the topology of T ) assume A in B ; ::_thesis: A in the topology of T then consider n being set such that A19: n in dom S and A20: A = S . n by FUNCT_1:def_3; reconsider n9 = n as Element of NAT by A5, A19; reconsider C = f .: (succ n) as Subset-Family of T by XBOOLE_1:1; A21: C is open proof let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in C or P is open ) assume P in C ; ::_thesis: P is open hence P is open by YELLOW_8:12; ::_thesis: verum end; succ n9 is finite ; then f .: (succ n) is finite ; then A22: meet C is open by A21, TOPS_2:20; A = meet (f .: (succ n)) by A5, A6, A19, A20; hence A in the topology of T by A22, PRE_TOPC:def_2; ::_thesis: verum end; for O being Subset of T st O is open & x in O holds ex A being Subset of T st ( A in B & A c= O ) proof let O be Subset of T; ::_thesis: ( O is open & x in O implies ex A being Subset of T st ( A in B & A c= O ) ) assume ( O is open & x in O ) ; ::_thesis: ex A being Subset of T st ( A in B & A c= O ) then consider A1 being Subset of T such that A23: A1 in B1 and A24: A1 c= O by YELLOW_8:def_1; consider n being set such that A25: n in dom f and A26: A1 = f . n by A3, A23, FUNCT_1:def_3; S . n in rng S by A5, A25, FUNCT_1:def_3; then reconsider A = S . n as Subset of T by A7; reconsider A = A as Subset of T ; take A ; ::_thesis: ( A in B & A c= O ) thus A in B by A5, A25, FUNCT_1:def_3; ::_thesis: A c= O n in succ n by ORDINAL1:6; then f . n in f .: (succ n) by A25, FUNCT_1:def_6; then meet (f .: (succ n)) c= A1 by A26, SETFAM_1:3; then S . n c= A1 by A6, A25; hence A c= O by A24, XBOOLE_1:1; ::_thesis: verum end; then reconsider B = B as Basis of x by A18, A10, A17, TOPS_2:64, YELLOW_8:def_1; take B ; ::_thesis: ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) take S ; ::_thesis: ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) thus dom S = NAT by A5; ::_thesis: ( rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) thus rng S = B ; ::_thesis: for n, m being Element of NAT st m >= n holds S . m c= S . n for n, m being Element of NAT st m >= n holds S . m c= S . n proof let n, m be Element of NAT ; ::_thesis: ( m >= n implies S . m c= S . n ) assume m >= n ; ::_thesis: S . m c= S . n then n + 1 <= m + 1 by XREAL_1:6; then n + 1 c= m + 1 by NAT_1:39; then succ n c= m + 1 by NAT_1:38; then succ n c= succ m by NAT_1:38; then A27: f .: (succ n) c= f .: (succ m) by RELAT_1:123; ( n in succ n & dom f = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then f . n in f .: (succ n) by FUNCT_1:def_6; then meet (f .: (succ m)) c= meet (f .: (succ n)) by A27, SETFAM_1:6; then S . m c= meet (f .: (succ n)) by A6; hence S . m c= S . n by A6; ::_thesis: verum end; hence for n, m being Element of NAT st m >= n holds S . m c= S . n ; ::_thesis: verum end; theorem :: FRECHET2:5 for T being non empty TopSpace st ( for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) holds T is T_1 proof let T be non empty TopSpace; ::_thesis: ( ( for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) implies T is T_1 ) assume A1: for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ; ::_thesis: T is T_1 assume not T is T_1 ; ::_thesis: contradiction then consider x1, x2 being Point of T, S being sequence of T such that A2: S = NAT --> x1 and A3: x1 <> x2 and A4: S is_convergent_to x2 by Lm3; S is_convergent_to x1 by A2, FRECHET:22; then A5: x1 in Lim S by FRECHET:def_5; x2 in Lim S by A4, FRECHET:def_5; hence contradiction by A1, A3, A5; ::_thesis: verum end; theorem Th6: :: FRECHET2:6 for T being non empty TopSpace st T is T_2 holds for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 proof let T be non empty TopSpace; ::_thesis: ( T is T_2 implies for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) assume A1: T is T_2 ; ::_thesis: for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 assume ex S being sequence of T ex x1, x2 being Point of T st ( x1 in Lim S & x2 in Lim S & not x1 = x2 ) ; ::_thesis: contradiction then consider S being sequence of T such that A2: ex x1, x2 being Point of T st ( x1 in Lim S & x2 in Lim S & x1 <> x2 ) ; consider x1, x2 being Point of T such that A3: x1 in Lim S and A4: x2 in Lim S and A5: x1 <> x2 by A2; consider U1, U2 being Subset of T such that A6: U1 is open and A7: U2 is open and A8: x1 in U1 and A9: x2 in U2 and A10: U1 misses U2 by A1, A5, PRE_TOPC:def_10; S is_convergent_to x1 by A3, FRECHET:def_5; then consider n1 being Element of NAT such that A11: for m being Element of NAT st n1 <= m holds S . m in U1 by A6, A8, FRECHET:def_3; S is_convergent_to x2 by A4, FRECHET:def_5; then consider n2 being Element of NAT such that A12: for m being Element of NAT st n2 <= m holds S . m in U2 by A7, A9, FRECHET:def_3; reconsider n = max (n1,n2) as Element of NAT ; A13: S . n in U1 by A11, XXREAL_0:25; A14: S . n in U2 by A12, XXREAL_0:25; U1 /\ U2 = {} by A10, XBOOLE_0:def_7; hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: FRECHET2:7 for T being non empty TopSpace st T is first-countable holds ( T is T_2 iff for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) proof let T be non empty TopSpace; ::_thesis: ( T is first-countable implies ( T is T_2 iff for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) ) assume A1: T is first-countable ; ::_thesis: ( T is T_2 iff for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) thus ( T is T_2 implies for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) by Th6; ::_thesis: ( ( for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ) implies T is T_2 ) assume A2: for S being sequence of T for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds x1 = x2 ; ::_thesis: T is T_2 assume not T is T_2 ; ::_thesis: contradiction then consider x1, x2 being Point of T such that A3: x1 <> x2 and A4: for U1, U2 being Subset of T st U1 is open & U2 is open & x1 in U1 & x2 in U2 holds U1 meets U2 by PRE_TOPC:def_10; consider B1 being Basis of x1 such that A5: ex S being Function st ( dom S = NAT & rng S = B1 & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) by A1, Lm5; consider B2 being Basis of x2 such that A6: ex S being Function st ( dom S = NAT & rng S = B2 & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) by A1, Lm5; consider S1 being Function such that A7: dom S1 = NAT and A8: rng S1 = B1 and A9: for n, m being Element of NAT st m >= n holds S1 . m c= S1 . n by A5; consider S2 being Function such that A10: dom S2 = NAT and A11: rng S2 = B2 and A12: for n, m being Element of NAT st m >= n holds S2 . m c= S2 . n by A6; defpred S1[ set , set ] means $2 in (S1 . $1) /\ (S2 . $1); A13: for n being set st n in NAT holds ex x being set st ( x in the carrier of T & S1[n,x] ) proof let n be set ; ::_thesis: ( n in NAT implies ex x being set st ( x in the carrier of T & S1[n,x] ) ) set x = the Element of (S1 . n) /\ (S2 . n); assume A14: n in NAT ; ::_thesis: ex x being set st ( x in the carrier of T & S1[n,x] ) then A15: S1 . n in B1 by A7, A8, FUNCT_1:def_3; then reconsider U1 = S1 . n as Subset of T ; A16: S2 . n in B2 by A10, A11, A14, FUNCT_1:def_3; then reconsider U2 = S2 . n as Subset of T ; take the Element of (S1 . n) /\ (S2 . n) ; ::_thesis: ( the Element of (S1 . n) /\ (S2 . n) in the carrier of T & S1[n, the Element of (S1 . n) /\ (S2 . n)] ) reconsider U1 = U1 as Subset of T ; reconsider U2 = U2 as Subset of T ; A17: ( U2 is open & x2 in U2 ) by A16, YELLOW_8:12; ( U1 is open & x1 in U1 ) by A15, YELLOW_8:12; then U1 meets U2 by A4, A17; then A18: U1 /\ U2 <> {} by XBOOLE_0:def_7; then the Element of (S1 . n) /\ (S2 . n) in U1 /\ U2 ; hence the Element of (S1 . n) /\ (S2 . n) in the carrier of T ; ::_thesis: S1[n, the Element of (S1 . n) /\ (S2 . n)] thus S1[n, the Element of (S1 . n) /\ (S2 . n)] by A18; ::_thesis: verum end; consider S being Function such that A19: ( dom S = NAT & rng S c= the carrier of T ) and A20: for n being set st n in NAT holds S1[n,S . n] from FUNCT_1:sch_5(A13); reconsider S = S as Function of NAT, the carrier of T by A19, FUNCT_2:def_1, RELSET_1:4; S is_convergent_to x2 proof let U2 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U2 is open or not x2 in U2 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U2 ) ) assume ( U2 is open & x2 in U2 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U2 ) then consider V2 being Subset of T such that A21: V2 in B2 and A22: V2 c= U2 by YELLOW_8:13; consider n being set such that A23: n in dom S2 and A24: V2 = S2 . n by A11, A21, FUNCT_1:def_3; reconsider n = n as Element of NAT by A10, A23; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S . b1 in U2 ) let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in U2 ) ( S . m in (S1 . m) /\ (S2 . m) & (S1 . m) /\ (S2 . m) c= S2 . m ) by A20, XBOOLE_1:17; then A25: S . m in S2 . m ; assume n <= m ; ::_thesis: S . m in U2 then S2 . m c= S2 . n by A12; then S . m in S2 . n by A25; hence S . m in U2 by A22, A24; ::_thesis: verum end; then A26: x2 in Lim S by FRECHET:def_5; S is_convergent_to x1 proof let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x1 in U1 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U1 ) ) assume ( U1 is open & x1 in U1 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U1 ) then consider V1 being Subset of T such that A27: V1 in B1 and A28: V1 c= U1 by YELLOW_8:13; consider n being set such that A29: n in dom S1 and A30: V1 = S1 . n by A8, A27, FUNCT_1:def_3; reconsider n = n as Element of NAT by A7, A29; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S . b1 in U1 ) let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in U1 ) ( S . m in (S1 . m) /\ (S2 . m) & (S1 . m) /\ (S2 . m) c= S1 . m ) by A20, XBOOLE_1:17; then A31: S . m in S1 . m ; assume n <= m ; ::_thesis: S . m in U1 then S1 . m c= S1 . n by A9; then S . m in S1 . n by A31; hence S . m in U1 by A28, A30; ::_thesis: verum end; then x1 in Lim S by FRECHET:def_5; hence contradiction by A2, A3, A26; ::_thesis: verum end; theorem :: FRECHET2:8 for T being non empty TopStruct for S being sequence of T st not S is convergent holds Lim S = {} proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T st not S is convergent holds Lim S = {} let S be sequence of T; ::_thesis: ( not S is convergent implies Lim S = {} ) assume A1: not S is convergent ; ::_thesis: Lim S = {} set x = the Element of Lim S; assume A2: Lim S <> {} ; ::_thesis: contradiction then the Element of Lim S in Lim S ; then reconsider x = the Element of Lim S as Point of T ; S is_convergent_to x by A2, FRECHET:def_5; hence contradiction by A1, FRECHET:def_4; ::_thesis: verum end; theorem Th9: :: FRECHET2:9 for T being non empty TopSpace for A being Subset of T st A is closed holds for S being sequence of T st rng S c= A holds Lim S c= A by FRECHET:24; theorem :: FRECHET2:10 for T being non empty TopStruct for S being sequence of T for x being Point of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x let S be sequence of T; ::_thesis: for x being Point of T st not S is_convergent_to x holds ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x let x be Point of T; ::_thesis: ( not S is_convergent_to x implies ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x ) assume not S is_convergent_to x ; ::_thesis: ex S1 being subsequence of S st for S2 being subsequence of S1 holds not S2 is_convergent_to x then consider A being Subset of T such that A1: ( A is open & x in A ) and A2: for n being Element of NAT ex m being Element of NAT st ( n <= m & not S . m in A ) by FRECHET:def_3; defpred S1[ set ] means not $1 in A; A3: for n being Element of NAT ex m being Element of NAT st ( n <= m & S1[S . m] ) by A2; consider S1 being subsequence of S such that A4: for n being Element of NAT holds S1[S1 . n] from VALUED_1:sch_1(A3); take S1 ; ::_thesis: for S2 being subsequence of S1 holds not S2 is_convergent_to x let S2 be subsequence of S1; ::_thesis: not S2 is_convergent_to x ex U1 being Subset of T st ( U1 is open & x in U1 & ( for n being Element of NAT ex m being Element of NAT st ( n <= m & not S2 . m in U1 ) ) ) proof take A ; ::_thesis: ( A is open & x in A & ( for n being Element of NAT ex m being Element of NAT st ( n <= m & not S2 . m in A ) ) ) consider NS being increasing sequence of NAT such that A5: S2 = S1 * NS by VALUED_0:def_17; thus ( A is open & x in A ) by A1; ::_thesis: for n being Element of NAT ex m being Element of NAT st ( n <= m & not S2 . m in A ) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n <= m & not S2 . m in A ) take n ; ::_thesis: ( n <= n & not S2 . n in A ) thus n <= n ; ::_thesis: not S2 . n in A n in NAT ; then n in dom S2 by NORMSP_1:12; then S2 . n = S1 . (NS . n) by A5, FUNCT_1:12; hence not S2 . n in A by A4; ::_thesis: verum end; hence not S2 is_convergent_to x by FRECHET:def_3; ::_thesis: verum end; begin theorem Th11: :: FRECHET2:11 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is continuous holds for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is continuous holds for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 let f be Function of T1,T2; ::_thesis: ( f is continuous implies for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) assume A1: f is continuous ; ::_thesis: for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 let S1 be sequence of T1; ::_thesis: for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 let S2 be sequence of T2; ::_thesis: ( S2 = f * S1 implies f .: (Lim S1) c= Lim S2 ) assume A2: S2 = f * S1 ; ::_thesis: f .: (Lim S1) c= Lim S2 let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (Lim S1) or y in Lim S2 ) assume A3: y in f .: (Lim S1) ; ::_thesis: y in Lim S2 then reconsider y9 = y as Point of T2 ; S2 is_convergent_to y9 proof let U2 be Subset of T2; :: according to FRECHET:def_3 ::_thesis: ( not U2 is open or not y9 in U2 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S2 . b2 in U2 ) ) assume that A4: U2 is open and A5: y9 in U2 ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S2 . b2 in U2 ) consider x being set such that A6: x in dom f and A7: x in Lim S1 and A8: y = f . x by A3, FUNCT_1:def_6; A9: x in f " U2 by A5, A6, A8, FUNCT_1:def_7; reconsider U1 = f " U2 as Subset of T1 ; [#] T2 <> {} ; then A10: U1 is open by A1, A4, TOPS_2:43; reconsider x = x as Point of T1 by A6; S1 is_convergent_to x by A7, FRECHET:def_5; then consider n being Element of NAT such that A11: for m being Element of NAT st n <= m holds S1 . m in f " U2 by A10, A9, FRECHET:def_3; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S2 . b1 in U2 ) let m be Element of NAT ; ::_thesis: ( not n <= m or S2 . m in U2 ) assume n <= m ; ::_thesis: S2 . m in U2 then S1 . m in f " U2 by A11; then A12: f . (S1 . m) in U2 by FUNCT_1:def_7; dom S1 = NAT by FUNCT_2:def_1; hence S2 . m in U2 by A2, A12, FUNCT_1:13; ::_thesis: verum end; hence y in Lim S2 by FRECHET:def_5; ::_thesis: verum end; theorem :: FRECHET2:12 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st T1 is sequential holds ( f is continuous iff for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st T1 is sequential holds ( f is continuous iff for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) let f be Function of T1,T2; ::_thesis: ( T1 is sequential implies ( f is continuous iff for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) ) assume A1: T1 is sequential ; ::_thesis: ( f is continuous iff for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) thus ( f is continuous implies for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) by Th11; ::_thesis: ( ( for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ) implies f is continuous ) assume A2: for S1 being sequence of T1 for S2 being sequence of T2 st S2 = f * S1 holds f .: (Lim S1) c= Lim S2 ; ::_thesis: f is continuous let B be Subset of T2; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or f " B is closed ) reconsider A = f " B as Subset of T1 ; assume A3: B is closed ; ::_thesis: f " B is closed for S being sequence of T1 st S is convergent & rng S c= A holds Lim S c= A proof reconsider B9 = B as Subset of T2 ; let S be sequence of T1; ::_thesis: ( S is convergent & rng S c= A implies Lim S c= A ) assume that S is convergent and A4: rng S c= A ; ::_thesis: Lim S c= A set S2 = f * S; rng (f * S) c= B9 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (f * S) or z in B9 ) assume z in rng (f * S) ; ::_thesis: z in B9 then consider n being set such that A5: n in dom (f * S) and A6: z = (f * S) . n by FUNCT_1:def_3; dom S = NAT by NORMSP_1:12; then S . n in rng S by A5, FUNCT_1:def_3; then f . (S . n) in B by A4, FUNCT_1:def_7; hence z in B9 by A5, A6, FUNCT_1:12; ::_thesis: verum end; then A7: Lim (f * S) c= B9 by A3, Th9; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim S or x in A ) A8: dom f = the carrier of T1 by FUNCT_2:def_1; A9: f .: (Lim S) c= Lim (f * S) by A2; assume A10: x in Lim S ; ::_thesis: x in A then f . x in f .: (Lim S) by A8, FUNCT_1:def_6; then f . x in Lim (f * S) by A9; hence x in A by A10, A8, A7, FUNCT_1:def_7; ::_thesis: verum end; hence f " B is closed by A1, FRECHET:def_7; ::_thesis: verum end; begin definition let T be non empty TopStruct ; let A be Subset of T; func Cl_Seq A -> Subset of T means :Def1: :: FRECHET2:def 1 for x being Point of T holds ( x in it iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ); existence ex b1 being Subset of T st for x being Point of T holds ( x in b1 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) proof defpred S1[ Point of T] means ex S being sequence of T st ( rng S c= A & $1 in Lim S ); reconsider X = { x where x is Point of T : S1[x] } as Subset of T from DOMAIN_1:sch_7(); reconsider X = X as Subset of T ; take X ; ::_thesis: for x being Point of T holds ( x in X iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) let x be Point of T; ::_thesis: ( x in X iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) thus ( x in X implies ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ::_thesis: ( ex S being sequence of T st ( rng S c= A & x in Lim S ) implies x in X ) proof assume x in X ; ::_thesis: ex S being sequence of T st ( rng S c= A & x in Lim S ) then ex x9 being Point of T st ( x = x9 & ex S being sequence of T st ( rng S c= A & x9 in Lim S ) ) ; hence ex S being sequence of T st ( rng S c= A & x in Lim S ) ; ::_thesis: verum end; assume ex S being sequence of T st ( rng S c= A & x in Lim S ) ; ::_thesis: x in X hence x in X ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of T st ( for x being Point of T holds ( x in b1 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ) & ( for x being Point of T holds ( x in b2 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ) holds b1 = b2 proof let A1, A2 be Subset of T; ::_thesis: ( ( for x being Point of T holds ( x in A1 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ) & ( for x being Point of T holds ( x in A2 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ) implies A1 = A2 ) assume that A1: for x being Point of T holds ( x in A1 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) and A2: for x being Point of T holds ( x in A2 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ; ::_thesis: A1 = A2 for x being Point of T holds ( x in A1 iff x in A2 ) proof let x be Point of T; ::_thesis: ( x in A1 iff x in A2 ) ( x in A1 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) by A1; hence ( x in A1 iff x in A2 ) by A2; ::_thesis: verum end; hence A1 = A2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def1 defines Cl_Seq FRECHET2:def_1_:_ for T being non empty TopStruct for A, b3 being Subset of T holds ( b3 = Cl_Seq A iff for x being Point of T holds ( x in b3 iff ex S being sequence of T st ( rng S c= A & x in Lim S ) ) ); theorem Th13: :: FRECHET2:13 for T being non empty TopStruct for A being Subset of T for S being sequence of T for x being Point of T st rng S c= A & x in Lim S holds x in Cl A proof let T be non empty TopStruct ; ::_thesis: for A being Subset of T for S being sequence of T for x being Point of T st rng S c= A & x in Lim S holds x in Cl A let A be Subset of T; ::_thesis: for S being sequence of T for x being Point of T st rng S c= A & x in Lim S holds x in Cl A let S be sequence of T; ::_thesis: for x being Point of T st rng S c= A & x in Lim S holds x in Cl A let x be Point of T; ::_thesis: ( rng S c= A & x in Lim S implies x in Cl A ) assume that A1: rng S c= A and A2: x in Lim S ; ::_thesis: x in Cl A for O being Subset of T st O is open & x in O holds A meets O proof let O be Subset of T; ::_thesis: ( O is open & x in O implies A meets O ) assume A3: O is open ; ::_thesis: ( not x in O or A meets O ) A4: S is_convergent_to x by A2, FRECHET:def_5; assume x in O ; ::_thesis: A meets O then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds S . m in O by A3, A4, FRECHET:def_3; n in NAT ; then n in dom S by NORMSP_1:12; then A6: S . n in rng S by FUNCT_1:def_3; S . n in O by A5; then S . n in A /\ O by A1, A6, XBOOLE_0:def_4; hence A meets O by XBOOLE_0:def_7; ::_thesis: verum end; hence x in Cl A by PRE_TOPC:def_7; ::_thesis: verum end; theorem Th14: :: FRECHET2:14 for T being non empty TopStruct for A being Subset of T holds Cl_Seq A c= Cl A proof let T be non empty TopStruct ; ::_thesis: for A being Subset of T holds Cl_Seq A c= Cl A let A be Subset of T; ::_thesis: Cl_Seq A c= Cl A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl_Seq A or x in Cl A ) assume A1: x in Cl_Seq A ; ::_thesis: x in Cl A then reconsider x9 = x as Point of T ; ex S being sequence of T st ( rng S c= A & x9 in Lim S ) by A1, Def1; hence x in Cl A by Th13; ::_thesis: verum end; theorem Th15: :: FRECHET2:15 for T being non empty TopStruct for S being sequence of T for S1 being subsequence of S for x being Point of T st S is_convergent_to x holds S1 is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for S1 being subsequence of S for x being Point of T st S is_convergent_to x holds S1 is_convergent_to x let S be sequence of T; ::_thesis: for S1 being subsequence of S for x being Point of T st S is_convergent_to x holds S1 is_convergent_to x let S1 be subsequence of S; ::_thesis: for x being Point of T st S is_convergent_to x holds S1 is_convergent_to x let x be Point of T; ::_thesis: ( S is_convergent_to x implies S1 is_convergent_to x ) assume A1: S is_convergent_to x ; ::_thesis: S1 is_convergent_to x let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x in U1 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S1 . b2 in U1 ) ) assume ( U1 is open & x in U1 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S1 . b2 in U1 ) then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds S . m in U1 by A1, FRECHET:def_3; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S1 . b1 in U1 ) let m be Element of NAT ; ::_thesis: ( not n <= m or S1 . m in U1 ) assume A3: n <= m ; ::_thesis: S1 . m in U1 m in NAT ; then A4: m in dom S1 by NORMSP_1:12; consider NS being increasing sequence of NAT such that A5: S1 = S * NS by VALUED_0:def_17; m <= NS . m by SEQM_3:14; then S . (NS . m) in U1 by A2, A3, XXREAL_0:2; hence S1 . m in U1 by A5, A4, FUNCT_1:12; ::_thesis: verum end; theorem Th16: :: FRECHET2:16 for T being non empty TopStruct for S being sequence of T for S1 being subsequence of S holds Lim S c= Lim S1 proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for S1 being subsequence of S holds Lim S c= Lim S1 let S be sequence of T; ::_thesis: for S1 being subsequence of S holds Lim S c= Lim S1 let S1 be subsequence of S; ::_thesis: Lim S c= Lim S1 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim S or x in Lim S1 ) assume A1: x in Lim S ; ::_thesis: x in Lim S1 then reconsider x9 = x as Point of T ; S is_convergent_to x9 by A1, FRECHET:def_5; then S1 is_convergent_to x9 by Th15; hence x in Lim S1 by FRECHET:def_5; ::_thesis: verum end; theorem Th17: :: FRECHET2:17 for T being non empty TopStruct holds Cl_Seq ({} T) = {} proof let T be non empty TopStruct ; ::_thesis: Cl_Seq ({} T) = {} set x = the Element of Cl_Seq ({} T); assume A1: Cl_Seq ({} T) <> {} ; ::_thesis: contradiction then the Element of Cl_Seq ({} T) in Cl_Seq ({} T) ; then reconsider x = the Element of Cl_Seq ({} T) as Point of T ; consider S being sequence of T such that A2: rng S c= {} T and x in Lim S by A1, Def1; rng S = {} by A2; then dom S = {} by RELAT_1:42; hence contradiction by NORMSP_1:12; ::_thesis: verum end; theorem Th18: :: FRECHET2:18 for T being non empty TopStruct for A being Subset of T holds A c= Cl_Seq A proof let T be non empty TopStruct ; ::_thesis: for A being Subset of T holds A c= Cl_Seq A let A be Subset of T; ::_thesis: A c= Cl_Seq A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Cl_Seq A ) assume A1: x in A ; ::_thesis: x in Cl_Seq A then reconsider x9 = x as Point of T ; ex S being sequence of T st ( rng S c= A & x9 in Lim S ) proof set S = NAT --> x9; take NAT --> x9 ; ::_thesis: ( rng (NAT --> x9) c= A & x9 in Lim (NAT --> x9) ) {x9} c= A proof let x99 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x99 in {x9} or x99 in A ) assume x99 in {x9} ; ::_thesis: x99 in A hence x99 in A by A1, TARSKI:def_1; ::_thesis: verum end; hence rng (NAT --> x9) c= A by FUNCOP_1:8; ::_thesis: x9 in Lim (NAT --> x9) NAT --> x9 is_convergent_to x9 by FRECHET:22; hence x9 in Lim (NAT --> x9) by FRECHET:def_5; ::_thesis: verum end; hence x in Cl_Seq A by Def1; ::_thesis: verum end; theorem Th19: :: FRECHET2:19 for T being non empty TopStruct for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B) proof let T be non empty TopStruct ; ::_thesis: for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B) let A, B be Subset of T; ::_thesis: (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B) thus (Cl_Seq A) \/ (Cl_Seq B) c= Cl_Seq (A \/ B) :: according to XBOOLE_0:def_10 ::_thesis: Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Cl_Seq A) \/ (Cl_Seq B) or x in Cl_Seq (A \/ B) ) assume A1: x in (Cl_Seq A) \/ (Cl_Seq B) ; ::_thesis: x in Cl_Seq (A \/ B) percases ( x in Cl_Seq A or x in Cl_Seq B ) by A1, XBOOLE_0:def_3; supposeA2: x in Cl_Seq A ; ::_thesis: x in Cl_Seq (A \/ B) then reconsider x9 = x as Point of T ; consider S being sequence of T such that A3: rng S c= A and A4: x9 in Lim S by A2, Def1; A c= A \/ B by XBOOLE_1:7; then rng S c= A \/ B by A3, XBOOLE_1:1; hence x in Cl_Seq (A \/ B) by A4, Def1; ::_thesis: verum end; supposeA5: x in Cl_Seq B ; ::_thesis: x in Cl_Seq (A \/ B) then reconsider x9 = x as Point of T ; consider S being sequence of T such that A6: rng S c= B and A7: x9 in Lim S by A5, Def1; B c= A \/ B by XBOOLE_1:7; then rng S c= A \/ B by A6, XBOOLE_1:1; hence x in Cl_Seq (A \/ B) by A7, Def1; ::_thesis: verum end; end; end; thus Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl_Seq (A \/ B) or x in (Cl_Seq A) \/ (Cl_Seq B) ) assume A8: x in Cl_Seq (A \/ B) ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq B) then reconsider x9 = x as Point of T ; consider S being sequence of T such that A9: rng S c= A \/ B and A10: x9 in Lim S by A8, Def1; consider S1 being subsequence of S such that A11: ( rng S1 c= A or rng S1 c= B ) by A9, Th4; A12: Lim S c= Lim S1 by Th16; percases ( rng S1 c= A or rng S1 c= B ) by A11; suppose rng S1 c= A ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq B) then x9 in Cl_Seq A by A10, A12, Def1; hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def_3; ::_thesis: verum end; suppose rng S1 c= B ; ::_thesis: x in (Cl_Seq A) \/ (Cl_Seq B) then x9 in Cl_Seq B by A10, A12, Def1; hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; theorem Th20: :: FRECHET2:20 for T being non empty TopStruct holds ( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A ) proof let T be non empty TopStruct ; ::_thesis: ( T is Frechet iff for A being Subset of T holds Cl A = Cl_Seq A ) thus ( T is Frechet implies for A being Subset of T holds Cl A = Cl_Seq A ) ::_thesis: ( ( for A being Subset of T holds Cl A = Cl_Seq A ) implies T is Frechet ) proof assume A1: T is Frechet ; ::_thesis: for A being Subset of T holds Cl A = Cl_Seq A let A be Subset of T; ::_thesis: Cl A = Cl_Seq A reconsider A9 = A as Subset of T ; thus Cl A c= Cl_Seq A :: according to XBOOLE_0:def_10 ::_thesis: Cl_Seq A c= Cl A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in Cl_Seq A ) assume A2: x in Cl A ; ::_thesis: x in Cl_Seq A then reconsider x9 = x as Point of T ; ex S being sequence of T st ( rng S c= A9 & x9 in Lim S ) by A1, A2, FRECHET:def_6; hence x in Cl_Seq A by Def1; ::_thesis: verum end; thus Cl_Seq A c= Cl A by Th14; ::_thesis: verum end; assume A3: for A being Subset of T holds Cl A = Cl_Seq A ; ::_thesis: T is Frechet let A be Subset of T; :: according to FRECHET:def_6 ::_thesis: for b1 being Element of the carrier of T holds ( not b1 in Cl A or ex b2 being Element of K10(K11(NAT, the carrier of T)) st ( rng b2 c= A & b1 in Lim b2 ) ) let x be Point of T; ::_thesis: ( not x in Cl A or ex b1 being Element of K10(K11(NAT, the carrier of T)) st ( rng b1 c= A & x in Lim b1 ) ) assume x in Cl A ; ::_thesis: ex b1 being Element of K10(K11(NAT, the carrier of T)) st ( rng b1 c= A & x in Lim b1 ) then x in Cl_Seq A by A3; hence ex b1 being Element of K10(K11(NAT, the carrier of T)) st ( rng b1 c= A & x in Lim b1 ) by Def1; ::_thesis: verum end; theorem Th21: :: FRECHET2:21 for T being non empty TopSpace st T is Frechet holds for A, B being Subset of T holds ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) proof let T be non empty TopSpace; ::_thesis: ( T is Frechet implies for A, B being Subset of T holds ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) ) assume A1: T is Frechet ; ::_thesis: for A, B being Subset of T holds ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) let A, B be Subset of T; ::_thesis: ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) thus ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) ) by Th17, Th18, Th19; ::_thesis: Cl_Seq (Cl_Seq A) = Cl_Seq A thus Cl_Seq (Cl_Seq A) = Cl_Seq (Cl A) by A1, Th20 .= Cl (Cl A) by A1, Th20 .= Cl_Seq A by A1, Th20 ; ::_thesis: verum end; theorem Th22: :: FRECHET2:22 for T being non empty TopSpace st T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) holds T is Frechet proof let T be non empty TopSpace; ::_thesis: ( T is sequential & ( for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ) implies T is Frechet ) assume A1: T is sequential ; ::_thesis: ( ex A being Subset of T st not Cl_Seq (Cl_Seq A) = Cl_Seq A or T is Frechet ) assume A2: for A being Subset of T holds Cl_Seq (Cl_Seq A) = Cl_Seq A ; ::_thesis: T is Frechet assume not T is Frechet ; ::_thesis: contradiction then consider A being Subset of T such that A3: ex x being Point of T st ( x in Cl A & ( for S being sequence of T st rng S c= A holds not x in Lim S ) ) by FRECHET:def_6; for Sq being sequence of T st Sq is convergent & rng Sq c= Cl_Seq A holds Lim Sq c= Cl_Seq A proof let Sq be sequence of T; ::_thesis: ( Sq is convergent & rng Sq c= Cl_Seq A implies Lim Sq c= Cl_Seq A ) assume that Sq is convergent and A4: rng Sq c= Cl_Seq A ; ::_thesis: Lim Sq c= Cl_Seq A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Lim Sq or y in Cl_Seq A ) assume A5: y in Lim Sq ; ::_thesis: y in Cl_Seq A then reconsider y9 = y as Point of T ; y9 in Cl_Seq (Cl_Seq A) by A4, A5, Def1; hence y in Cl_Seq A by A2; ::_thesis: verum end; then A6: Cl_Seq A is closed by A1, FRECHET:def_7; consider x being Point of T such that A7: x in Cl A and A8: for S being sequence of T st rng S c= A holds not x in Lim S by A3; A c= Cl_Seq A by Th18; then x in Cl_Seq A by A7, A6, PRE_TOPC:15; hence contradiction by A8, Def1; ::_thesis: verum end; theorem :: FRECHET2:23 for T being non empty TopSpace st T is sequential holds ( T is Frechet iff for A, B being Subset of T holds ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) ) by Th21, Th22; begin definition let T be non empty TopSpace; let S be sequence of T; assume A1: ex x being Point of T st Lim S = {x} ; func lim S -> Point of T means :Def2: :: FRECHET2:def 2 S is_convergent_to it; existence ex b1 being Point of T st S is_convergent_to b1 proof consider x being Point of T such that A2: Lim S = {x} by A1; take x ; ::_thesis: S is_convergent_to x x in {x} by TARSKI:def_1; hence S is_convergent_to x by A2, FRECHET:def_5; ::_thesis: verum end; uniqueness for b1, b2 being Point of T st S is_convergent_to b1 & S is_convergent_to b2 holds b1 = b2 proof let x1, x2 be Point of T; ::_thesis: ( S is_convergent_to x1 & S is_convergent_to x2 implies x1 = x2 ) assume that A3: S is_convergent_to x1 and A4: S is_convergent_to x2 ; ::_thesis: x1 = x2 consider x being Point of T such that A5: Lim S = {x} by A1; A6: x2 in {x} by A4, A5, FRECHET:def_5; x1 in Lim S by A3, FRECHET:def_5; then x1 = x by A5, TARSKI:def_1; hence x1 = x2 by A6, TARSKI:def_1; ::_thesis: verum end; end; :: deftheorem Def2 defines lim FRECHET2:def_2_:_ for T being non empty TopSpace for S being sequence of T st ex x being Point of T st Lim S = {x} holds for b3 being Point of T holds ( b3 = lim S iff S is_convergent_to b3 ); theorem Th24: :: FRECHET2:24 for T being non empty TopSpace st T is T_2 holds for S being sequence of T st S is convergent holds ex x being Point of T st Lim S = {x} proof let T be non empty TopSpace; ::_thesis: ( T is T_2 implies for S being sequence of T st S is convergent holds ex x being Point of T st Lim S = {x} ) assume A1: T is T_2 ; ::_thesis: for S being sequence of T st S is convergent holds ex x being Point of T st Lim S = {x} let S be sequence of T; ::_thesis: ( S is convergent implies ex x being Point of T st Lim S = {x} ) assume S is convergent ; ::_thesis: ex x being Point of T st Lim S = {x} then consider x being Point of T such that A2: S is_convergent_to x by FRECHET:def_4; take x ; ::_thesis: Lim S = {x} A3: x in Lim S by A2, FRECHET:def_5; thus Lim S c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= Lim S proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Lim S or y in {x} ) assume A4: y in Lim S ; ::_thesis: y in {x} then reconsider y9 = y as Point of T ; y9 = x by A1, A3, A4, Th6; hence y in {x} by TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x} or y in Lim S ) assume y in {x} ; ::_thesis: y in Lim S hence y in Lim S by A3, TARSKI:def_1; ::_thesis: verum end; theorem Th25: :: FRECHET2:25 for T being non empty TopSpace st T is T_2 holds for S being sequence of T for x being Point of T holds ( S is_convergent_to x iff ( S is convergent & x = lim S ) ) proof let T be non empty TopSpace; ::_thesis: ( T is T_2 implies for S being sequence of T for x being Point of T holds ( S is_convergent_to x iff ( S is convergent & x = lim S ) ) ) assume A1: T is T_2 ; ::_thesis: for S being sequence of T for x being Point of T holds ( S is_convergent_to x iff ( S is convergent & x = lim S ) ) let S be sequence of T; ::_thesis: for x being Point of T holds ( S is_convergent_to x iff ( S is convergent & x = lim S ) ) let x be Point of T; ::_thesis: ( S is_convergent_to x iff ( S is convergent & x = lim S ) ) thus ( S is_convergent_to x implies ( S is convergent & x = lim S ) ) ::_thesis: ( S is convergent & x = lim S implies S is_convergent_to x ) proof assume A2: S is_convergent_to x ; ::_thesis: ( S is convergent & x = lim S ) hence S is convergent by FRECHET:def_4; ::_thesis: x = lim S then ex y being Point of T st Lim S = {y} by A1, Th24; hence x = lim S by A2, Def2; ::_thesis: verum end; assume that A3: S is convergent and A4: x = lim S ; ::_thesis: S is_convergent_to x ex x being Point of T st Lim S = {x} by A1, A3, Th24; hence S is_convergent_to x by A4, Def2; ::_thesis: verum end; theorem :: FRECHET2:26 for M being MetrStruct for S being sequence of M holds S is sequence of (TopSpaceMetr M) proof let M be MetrStruct ; ::_thesis: for S being sequence of M holds S is sequence of (TopSpaceMetr M) let S be sequence of M; ::_thesis: S is sequence of (TopSpaceMetr M) the carrier of M = the carrier of (TopSpaceMetr M) by TOPMETR:12; hence S is sequence of (TopSpaceMetr M) ; ::_thesis: verum end; theorem :: FRECHET2:27 for M being non empty MetrStruct for S being sequence of (TopSpaceMetr M) holds S is sequence of M by TOPMETR:12; theorem Th28: :: FRECHET2:28 for M being non empty MetrSpace for S being sequence of M for x being Point of M for S9 being sequence of (TopSpaceMetr M) for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) proof let M be non empty MetrSpace; ::_thesis: for S being sequence of M for x being Point of M for S9 being sequence of (TopSpaceMetr M) for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) let S be sequence of M; ::_thesis: for x being Point of M for S9 being sequence of (TopSpaceMetr M) for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) let x be Point of M; ::_thesis: for S9 being sequence of (TopSpaceMetr M) for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) let S9 be sequence of (TopSpaceMetr M); ::_thesis: for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) let x9 be Point of (TopSpaceMetr M); ::_thesis: ( S = S9 & x = x9 implies ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) ) assume that A1: S = S9 and A2: x = x9 ; ::_thesis: ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) thus ( S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9 ) ::_thesis: ( S9 is_convergent_to x9 implies S is_convergent_in_metrspace_to x ) proof assume A3: S is_convergent_in_metrspace_to x ; ::_thesis: S9 is_convergent_to x9 let U1 be Subset of (TopSpaceMetr M); :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x9 in U1 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S9 . b2 in U1 ) ) assume ( U1 is open & x9 in U1 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S9 . b2 in U1 ) then consider r being real number such that A4: r > 0 and A5: Ball (x,r) c= U1 by A2, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; Ball (x,r) contains_almost_all_sequence S by A3, A4, METRIC_6:15; then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds S . m in Ball (x,r) by METRIC_6:def_5; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S9 . b1 in U1 ) let m be Element of NAT ; ::_thesis: ( not n <= m or S9 . m in U1 ) assume n <= m ; ::_thesis: S9 . m in U1 then S . m in Ball (x,r) by A6; hence S9 . m in U1 by A1, A5; ::_thesis: verum end; assume A7: S9 is_convergent_to x9 ; ::_thesis: S is_convergent_in_metrspace_to x for V being Subset of M st x in V & V in Family_open_set M holds V contains_almost_all_sequence S proof let V be Subset of M; ::_thesis: ( x in V & V in Family_open_set M implies V contains_almost_all_sequence S ) assume that A8: x in V and A9: V in Family_open_set M ; ::_thesis: V contains_almost_all_sequence S reconsider V9 = V as Subset of (TopSpaceMetr M) by TOPMETR:12; reconsider V9 = V9 as Subset of (TopSpaceMetr M) ; V9 in the topology of (TopSpaceMetr M) by A9, TOPMETR:12; then V9 is open by PRE_TOPC:def_2; then consider n being Element of NAT such that A10: for m being Element of NAT st n <= m holds S9 . m in V9 by A2, A7, A8, FRECHET:def_3; take n ; :: according to METRIC_6:def_5 ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or S . b1 in V ) let m be Element of NAT ; ::_thesis: ( not n <= m or S . m in V ) assume n <= m ; ::_thesis: S . m in V hence S . m in V by A1, A10; ::_thesis: verum end; hence S is_convergent_in_metrspace_to x by METRIC_6:17; ::_thesis: verum end; theorem :: FRECHET2:29 for M being non empty MetrSpace for Sm being sequence of M for St being sequence of (TopSpaceMetr M) st Sm = St holds ( Sm is convergent iff St is convergent ) proof let M be non empty MetrSpace; ::_thesis: for Sm being sequence of M for St being sequence of (TopSpaceMetr M) st Sm = St holds ( Sm is convergent iff St is convergent ) let Sm be sequence of M; ::_thesis: for St being sequence of (TopSpaceMetr M) st Sm = St holds ( Sm is convergent iff St is convergent ) let St be sequence of (TopSpaceMetr M); ::_thesis: ( Sm = St implies ( Sm is convergent iff St is convergent ) ) assume A1: Sm = St ; ::_thesis: ( Sm is convergent iff St is convergent ) thus ( Sm is convergent implies St is convergent ) ::_thesis: ( St is convergent implies Sm is convergent ) proof assume Sm is convergent ; ::_thesis: St is convergent then consider x being Point of M such that A2: Sm is_convergent_in_metrspace_to x by METRIC_6:10; reconsider x9 = x as Point of (TopSpaceMetr M) by TOPMETR:12; St is_convergent_to x9 by A1, A2, Th28; hence St is convergent by FRECHET:def_4; ::_thesis: verum end; assume St is convergent ; ::_thesis: Sm is convergent then consider x9 being Point of (TopSpaceMetr M) such that A3: St is_convergent_to x9 by FRECHET:def_4; reconsider x = x9 as Point of M by TOPMETR:12; Sm is_convergent_in_metrspace_to x by A1, A3, Th28; hence Sm is convergent by METRIC_6:9; ::_thesis: verum end; theorem :: FRECHET2:30 for M being non empty MetrSpace for Sm being sequence of M for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds lim Sm = lim St proof let M be non empty MetrSpace; ::_thesis: for Sm being sequence of M for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds lim Sm = lim St let Sm be sequence of M; ::_thesis: for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds lim Sm = lim St let St be sequence of (TopSpaceMetr M); ::_thesis: ( Sm = St & Sm is convergent implies lim Sm = lim St ) assume that A1: Sm = St and A2: Sm is convergent ; ::_thesis: lim Sm = lim St set x = lim Sm; reconsider x9 = lim Sm as Point of (TopSpaceMetr M) by TOPMETR:12; Sm is_convergent_in_metrspace_to lim Sm by A2, METRIC_6:12; then ( TopSpaceMetr M is T_2 & St is_convergent_to x9 ) by A1, Th28, PCOMPS_1:34; hence lim Sm = lim St by Th25; ::_thesis: verum end; begin definition let T be TopStruct ; let S be sequence of T; let x be Point of T; predx is_a_cluster_point_of S means :Def3: :: FRECHET2:def 3 for O being Subset of T for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & S . m in O ); end; :: deftheorem Def3 defines is_a_cluster_point_of FRECHET2:def_3_:_ for T being TopStruct for S being sequence of T for x being Point of T holds ( x is_a_cluster_point_of S iff for O being Subset of T for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & S . m in O ) ); theorem Th31: :: FRECHET2:31 for T being non empty TopStruct for S being sequence of T for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x is_a_cluster_point_of S proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x is_a_cluster_point_of S let S be sequence of T; ::_thesis: for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds x is_a_cluster_point_of S let x be Point of T; ::_thesis: ( ex S1 being subsequence of S st S1 is_convergent_to x implies x is_a_cluster_point_of S ) given S1 being subsequence of S such that A1: S1 is_convergent_to x ; ::_thesis: x is_a_cluster_point_of S let O be Subset of T; :: according to FRECHET2:def_3 ::_thesis: for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & S . m in O ) let n be Element of NAT ; ::_thesis: ( O is open & x in O implies ex m being Element of NAT st ( n <= m & S . m in O ) ) assume ( O is open & x in O ) ; ::_thesis: ex m being Element of NAT st ( n <= m & S . m in O ) then consider n1 being Element of NAT such that A2: for m being Element of NAT st n1 <= m holds S1 . m in O by A1, FRECHET:def_3; set n2 = max (n1,n); A3: S1 . (max (n1,n)) in O by A2, XXREAL_0:25; consider NS being increasing sequence of NAT such that A4: S1 = S * NS by VALUED_0:def_17; take NS . (max (n1,n)) ; ::_thesis: ( n <= NS . (max (n1,n)) & S . (NS . (max (n1,n))) in O ) ( n <= max (n1,n) & max (n1,n) <= NS . (max (n1,n)) ) by SEQM_3:14, XXREAL_0:25; hence n <= NS . (max (n1,n)) by XXREAL_0:2; ::_thesis: S . (NS . (max (n1,n))) in O max (n1,n) in NAT ; then max (n1,n) in dom NS by FUNCT_2:def_1; hence S . (NS . (max (n1,n))) in O by A4, A3, FUNCT_1:13; ::_thesis: verum end; theorem :: FRECHET2:32 for T being non empty TopStruct for S being sequence of T for x being Point of T st S is_convergent_to x holds x is_a_cluster_point_of S proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T st S is_convergent_to x holds x is_a_cluster_point_of S let S be sequence of T; ::_thesis: for x being Point of T st S is_convergent_to x holds x is_a_cluster_point_of S let x be Point of T; ::_thesis: ( S is_convergent_to x implies x is_a_cluster_point_of S ) assume A1: S is_convergent_to x ; ::_thesis: x is_a_cluster_point_of S ex S1 being subsequence of S st S1 is_convergent_to x proof reconsider S1 = S as subsequence of S by VALUED_0:19; take S1 ; ::_thesis: S1 is_convergent_to x thus S1 is_convergent_to x by A1; ::_thesis: verum end; hence x is_a_cluster_point_of S by Th31; ::_thesis: verum end; theorem Th33: :: FRECHET2:33 for T being non empty TopStruct for S being sequence of T for x being Point of T for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds S is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds S is_convergent_to x let S be sequence of T; ::_thesis: for x being Point of T for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds S is_convergent_to x let x be Point of T; ::_thesis: for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds S is_convergent_to x let Y be Subset of T; ::_thesis: ( Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y implies S is_convergent_to x ) assume that A1: Y = { y where y is Point of T : x in Cl {y} } and A2: rng S c= Y ; ::_thesis: S is_convergent_to x let U1 be Subset of T; :: according to FRECHET:def_3 ::_thesis: ( not U1 is open or not x in U1 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U1 ) ) assume A3: ( U1 is open & x in U1 ) ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or S . b2 in U1 ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or S . b1 in U1 ) let m be Element of NAT ; ::_thesis: ( not 0 <= m or S . m in U1 ) m in NAT ; then m in dom S by NORMSP_1:12; then S . m in rng S by FUNCT_1:def_3; then S . m in Y by A2; then consider y being Point of T such that A4: y = S . m and A5: x in Cl {y} by A1; assume 0 <= m ; ::_thesis: S . m in U1 {y} meets U1 by A3, A5, PRE_TOPC:def_7; hence S . m in U1 by A4, ZFMISC_1:50; ::_thesis: verum end; theorem Th34: :: FRECHET2:34 for T being non empty TopStruct for S being sequence of T for x, y being Point of T st ( for n being Element of NAT holds ( S . n = y & S is_convergent_to x ) ) holds x in Cl {y} proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x, y being Point of T st ( for n being Element of NAT holds ( S . n = y & S is_convergent_to x ) ) holds x in Cl {y} let S be sequence of T; ::_thesis: for x, y being Point of T st ( for n being Element of NAT holds ( S . n = y & S is_convergent_to x ) ) holds x in Cl {y} let x, y be Point of T; ::_thesis: ( ( for n being Element of NAT holds ( S . n = y & S is_convergent_to x ) ) implies x in Cl {y} ) assume A1: for n being Element of NAT holds ( S . n = y & S is_convergent_to x ) ; ::_thesis: x in Cl {y} for G being Subset of T st G is open & x in G holds {y} meets G proof let G be Subset of T; ::_thesis: ( G is open & x in G implies {y} meets G ) assume A2: G is open ; ::_thesis: ( not x in G or {y} meets G ) assume x in G ; ::_thesis: {y} meets G then consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds S . m in G by A1, A2, FRECHET:def_3; S . n in G by A3; then A4: y in G by A1; y in {y} by TARSKI:def_1; then y in {y} /\ G by A4, XBOOLE_0:def_4; hence {y} meets G by XBOOLE_0:def_7; ::_thesis: verum end; hence x in Cl {y} by PRE_TOPC:def_7; ::_thesis: verum end; theorem Th35: :: FRECHET2:35 for T being non empty TopStruct for x being Point of T for Y being Subset of T for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds ex S1 being subsequence of S st S1 is one-to-one proof let T be non empty TopStruct ; ::_thesis: for x being Point of T for Y being Subset of T for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds ex S1 being subsequence of S st S1 is one-to-one let x be Point of T; ::_thesis: for Y being Subset of T for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds ex S1 being subsequence of S st S1 is one-to-one let Y be Subset of T; ::_thesis: for S being sequence of T st Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x holds ex S1 being subsequence of S st S1 is one-to-one let S be sequence of T; ::_thesis: ( Y = { y where y is Point of T : x in Cl {y} } & rng S misses Y & S is_convergent_to x implies ex S1 being subsequence of S st S1 is one-to-one ) assume that A1: Y = { y where y is Point of T : x in Cl {y} } and A2: (rng S) /\ Y = {} and A3: S is_convergent_to x ; :: according to XBOOLE_0:def_7 ::_thesis: ex S1 being subsequence of S st S1 is one-to-one defpred S1[ Element of NAT , set , set ] means ( $3 in NAT & ( for n1, n2, m being Element of NAT st n1 = $2 & n2 = $3 & n2 <= m holds S . m <> S . n1 ) ); A4: for z being set st z in rng S holds ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds z <> S . m proof let z be set ; ::_thesis: ( z in rng S implies ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds z <> S . m ) defpred S2[ set ] means $1 = z; assume A5: z in rng S ; ::_thesis: ex n0 being Element of NAT st for m being Element of NAT st n0 <= m holds z <> S . m then reconsider z9 = z as Point of T ; assume for n0 being Element of NAT ex m being Element of NAT st ( n0 <= m & z = S . m ) ; ::_thesis: contradiction then A6: for n being Element of NAT ex m being Element of NAT st ( n <= m & S2[S . m] ) ; ex S1 being subsequence of S st for n being Element of NAT holds S2[S1 . n] from VALUED_1:sch_1(A6); then x in Cl {z9} by A3, Th15, Th34; then z9 in Y by A1; hence contradiction by A2, A5, XBOOLE_0:def_4; ::_thesis: verum end; A7: for n being Element of NAT for z1 being set ex z2 being set st S1[n,z1,z2] proof let n be Element of NAT ; ::_thesis: for z1 being set ex z2 being set st S1[n,z1,z2] let z1 be set ; ::_thesis: ex z2 being set st S1[n,z1,z2] percases ( not z1 in NAT or z1 in NAT ) ; supposeA8: not z1 in NAT ; ::_thesis: ex z2 being set st S1[n,z1,z2] take 0 ; ::_thesis: S1[n,z1, 0 ] thus 0 in NAT ; ::_thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = 0 & n2 <= m holds S . m <> S . n1 let n1, n2, m be Element of NAT ; ::_thesis: ( n1 = z1 & n2 = 0 & n2 <= m implies S . m <> S . n1 ) assume that A9: n1 = z1 and n2 = 0 and n2 <= m ; ::_thesis: S . m <> S . n1 thus S . m <> S . n1 by A8, A9; ::_thesis: verum end; suppose z1 in NAT ; ::_thesis: ex z2 being set st S1[n,z1,z2] then z1 in dom S by NORMSP_1:12; then S . z1 in rng S by FUNCT_1:def_3; then consider n0 being Element of NAT such that A10: for m being Element of NAT st n0 <= m holds S . z1 <> S . m by A4; take n0 ; ::_thesis: S1[n,z1,n0] thus n0 in NAT ; ::_thesis: for n1, n2, m being Element of NAT st n1 = z1 & n2 = n0 & n2 <= m holds S . m <> S . n1 let n1, n2, m be Element of NAT ; ::_thesis: ( n1 = z1 & n2 = n0 & n2 <= m implies S . m <> S . n1 ) assume ( n1 = z1 & n2 = n0 & n2 <= m ) ; ::_thesis: S . m <> S . n1 hence S . m <> S . n1 by A10; ::_thesis: verum end; end; end; consider f being Function such that A11: dom f = NAT and A12: f . 0 = 0 and A13: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_1(A7); A14: for n being Element of NAT holds f . n is Element of NAT proof let n be Element of NAT ; ::_thesis: f . n is Element of NAT percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: f . n is Element of NAT hence f . n is Element of NAT by A12; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: f . n is Element of NAT then 0 < n by NAT_1:3; then 0 + 1 < n + 1 by XREAL_1:6; then 1 <= n by NAT_1:13; then reconsider n1 = n - 1 as Element of NAT by INT_1:5; n1 + 1 = n ; hence f . n is Element of NAT by A13; ::_thesis: verum end; end; end; then for n being Element of NAT holds f . n is real ; then reconsider f = f as Real_Sequence by A11, SEQ_1:2; f is increasing proof let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not f . (n + 1) <= f . n reconsider n2 = f . (n + 1) as Element of NAT by A14; reconsider n1 = f . n as Element of NAT by A14; assume f . n >= f . (n + 1) ; ::_thesis: contradiction then n2 <= n1 ; then S . n1 <> S . n1 by A13; hence contradiction ; ::_thesis: verum end; then reconsider f = f as increasing sequence of NAT by A14, SEQM_3:13; take S1 = S * f; ::_thesis: S1 is one-to-one A15: for n1, n2 being Element of NAT st n1 < n2 holds S1 . n1 <> S1 . n2 proof let n1, n2 be Element of NAT ; ::_thesis: ( n1 < n2 implies S1 . n1 <> S1 . n2 ) reconsider n19 = f . n1 as Element of NAT ; n2 in NAT ; then n2 in dom S1 by NORMSP_1:12; then A16: S . (f . n2) = S1 . n2 by FUNCT_1:12; assume n1 < n2 ; ::_thesis: S1 . n1 <> S1 . n2 then A17: n1 + 1 <= n2 by NAT_1:13; f . (n1 + 1) <= f . n2 proof percases ( n1 + 1 = n2 or n1 + 1 <> n2 ) ; suppose n1 + 1 = n2 ; ::_thesis: f . (n1 + 1) <= f . n2 hence f . (n1 + 1) <= f . n2 ; ::_thesis: verum end; suppose n1 + 1 <> n2 ; ::_thesis: f . (n1 + 1) <= f . n2 then n1 + 1 < n2 by A17, XXREAL_0:1; hence f . (n1 + 1) <= f . n2 by SEQM_3:1; ::_thesis: verum end; end; end; then A18: S . (f . n2) <> S . n19 by A13; n1 in NAT ; then n1 in dom S1 by NORMSP_1:12; hence S1 . n1 <> S1 . n2 by A18, A16, FUNCT_1:12; ::_thesis: verum end; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom S1 or not x2 in dom S1 or not S1 . x1 = S1 . x2 or x1 = x2 ) assume that A19: x1 in dom S1 and A20: x2 in dom S1 and A21: S1 . x1 = S1 . x2 ; ::_thesis: x1 = x2 reconsider n2 = x2 as Element of NAT by A20; reconsider n1 = x1 as Element of NAT by A19; assume A22: x1 <> x2 ; ::_thesis: contradiction percases ( n1 < n2 or n2 < n1 ) by A22, XXREAL_0:1; suppose n1 < n2 ; ::_thesis: contradiction hence contradiction by A21, A15; ::_thesis: verum end; suppose n2 < n1 ; ::_thesis: contradiction hence contradiction by A21, A15; ::_thesis: verum end; end; end; theorem Th36: :: FRECHET2:36 for T being non empty TopStruct for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds ex P being Permutation of NAT st S2 * P is subsequence of S1 proof let T be non empty TopStruct ; ::_thesis: for S1, S2 being sequence of T st rng S2 c= rng S1 & S2 is one-to-one holds ex P being Permutation of NAT st S2 * P is subsequence of S1 let S1, S2 be sequence of T; ::_thesis: ( rng S2 c= rng S1 & S2 is one-to-one implies ex P being Permutation of NAT st S2 * P is subsequence of S1 ) assume that A1: rng S2 c= rng S1 and A2: S2 is one-to-one ; ::_thesis: ex P being Permutation of NAT st S2 * P is subsequence of S1 defpred S1[ set , set ] means S2 . $1 = S1 . $2; A3: for n being set st n in NAT holds ex u being set st ( u in NAT & S1[n,u] ) proof let n be set ; ::_thesis: ( n in NAT implies ex u being set st ( u in NAT & S1[n,u] ) ) assume n in NAT ; ::_thesis: ex u being set st ( u in NAT & S1[n,u] ) then n in dom S2 by NORMSP_1:12; then S2 . n in rng S2 by FUNCT_1:def_3; then consider m being set such that A4: m in dom S1 and A5: S2 . n = S1 . m by A1, FUNCT_1:def_3; take m ; ::_thesis: ( m in NAT & S1[n,m] ) thus m in NAT by A4; ::_thesis: S1[n,m] thus S1[n,m] by A5; ::_thesis: verum end; consider f being Function such that A6: dom f = NAT and A7: rng f c= NAT and A8: for n being set st n in NAT holds S1[n,f . n] from FUNCT_1:sch_5(A3); reconsider A = rng f as non empty Subset of NAT by A6, A7, RELAT_1:42; defpred S2[ Element of NAT , set , set ] means for B being non empty Subset of NAT for m being Element of NAT st m = $2 & B = { k where k is Element of NAT : ( k in rng f & k > m ) } holds $3 = min B; A9: f is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A10: x1 in dom f and A11: x2 in dom f and A12: f . x1 = f . x2 ; ::_thesis: x1 = x2 S2 . x2 = S1 . (f . x2) by A6, A8, A11; then A13: S2 . x1 = S2 . x2 by A6, A8, A10, A12; ( x1 in dom S2 & x2 in dom S2 ) by A6, A10, A11, NORMSP_1:12; hence x1 = x2 by A2, A13, FUNCT_1:def_4; ::_thesis: verum end; A14: for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } <> {} proof let m be Element of NAT ; ::_thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } <> {} assume A15: { k where k is Element of NAT : ( k in rng f & k > m ) } = {} ; ::_thesis: contradiction rng f c= m + 1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in m + 1 ) assume A16: x in rng f ; ::_thesis: x in m + 1 then reconsider x9 = x as Element of NAT by A7; x9 < m + 1 proof assume x9 >= m + 1 ; ::_thesis: contradiction then x9 > m by NAT_1:13; then x9 in { k where k is Element of NAT : ( k in rng f & k > m ) } by A16; hence contradiction by A15; ::_thesis: verum end; then x9 in { x99 where x99 is Element of NAT : x99 < m + 1 } ; hence x in m + 1 by AXIOMS:4; ::_thesis: verum end; then rng f is finite ; hence contradiction by A6, A9, CARD_1:59; ::_thesis: verum end; A17: for m being Element of NAT holds { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT proof let m be Element of NAT ; ::_thesis: { k where k is Element of NAT : ( k in rng f & k > m ) } c= NAT let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { k where k is Element of NAT : ( k in rng f & k > m ) } or z in NAT ) assume z in { k where k is Element of NAT : ( k in rng f & k > m ) } ; ::_thesis: z in NAT then ex k being Element of NAT st ( k = z & k in rng f & k > m ) ; hence z in NAT ; ::_thesis: verum end; A18: for n being Element of NAT for x being set ex y being set st S2[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being set ex y being set st S2[n,x,y] let x be set ; ::_thesis: ex y being set st S2[n,x,y] percases ( x in NAT or not x in NAT ) ; suppose x in NAT ; ::_thesis: ex y being set st S2[n,x,y] then reconsider x9 = x as Element of NAT ; set B = { k where k is Element of NAT : ( k in rng f & k > x9 ) } ; reconsider B = { k where k is Element of NAT : ( k in rng f & k > x9 ) } as Subset of NAT by A17; reconsider B = B as non empty Subset of NAT by A14; take min B ; ::_thesis: S2[n,x, min B] let B9 be non empty Subset of NAT; ::_thesis: for m being Element of NAT st m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } holds min B = min B9 let m be Element of NAT ; ::_thesis: ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } implies min B = min B9 ) assume ( m = x & B9 = { k where k is Element of NAT : ( k in rng f & k > m ) } ) ; ::_thesis: min B = min B9 hence min B = min B9 ; ::_thesis: verum end; supposeA19: not x in NAT ; ::_thesis: ex y being set st S2[n,x,y] take 0 ; ::_thesis: S2[n,x, 0 ] let B be non empty Subset of NAT; ::_thesis: for m being Element of NAT st m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } holds 0 = min B let m be Element of NAT ; ::_thesis: ( m = x & B = { k where k is Element of NAT : ( k in rng f & k > m ) } implies 0 = min B ) assume that A20: m = x and B = { k where k is Element of NAT : ( k in rng f & k > m ) } ; ::_thesis: 0 = min B thus 0 = min B by A19, A20; ::_thesis: verum end; end; end; consider g being Function such that A21: dom g = NAT and A22: g . 0 = min A and A23: for n being Element of NAT holds S2[n,g . n,g . (n + 1)] from RECDEF_1:sch_1(A18); defpred S3[ Element of NAT ] means g . $1 in NAT ; A24: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) assume g . k in NAT ; ::_thesis: S3[k + 1] then reconsider m = g . k as Element of NAT ; set B = { l where l is Element of NAT : ( l in rng f & l > m ) } ; reconsider B = { l where l is Element of NAT : ( l in rng f & l > m ) } as Subset of NAT by A17; reconsider B = B as non empty Subset of NAT by A14; g . (k + 1) = min B by A23; hence S3[k + 1] ; ::_thesis: verum end; A25: S3[ 0 ] by A22; A26: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A25, A24); for n being Element of NAT holds g . n is real proof let n be Element of NAT ; ::_thesis: g . n is real g . n in NAT by A26; then reconsider w = g . n as Element of REAL ; w is real ; hence g . n is real ; ::_thesis: verum end; then reconsider g1 = g as Real_Sequence by A21, SEQ_1:2; A27: g1 is increasing proof let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not g1 . (n + 1) <= g1 . n reconsider m = g . n as Element of NAT by A26; reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A14, A17; g1 . (n + 1) = min B by A23; then g1 . (n + 1) in B by XXREAL_2:def_7; then ex k being Element of NAT st ( k = g1 . (n + 1) & k in rng f & k > m ) ; hence not g1 . (n + 1) <= g1 . n ; ::_thesis: verum end; A28: rng g c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in NAT ) assume y in rng g ; ::_thesis: y in NAT then consider x being set such that A29: x in dom g and A30: y = g . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A21, A29; g . x in NAT by A26; hence y in NAT by A30; ::_thesis: verum end; then reconsider g1 = g1 as increasing sequence of NAT by A21, A27, RELSET_1:4; A31: g1 is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom g1 or not x2 in dom g1 or not g1 . x1 = g1 . x2 or x1 = x2 ) assume that A32: x1 in dom g1 and A33: x2 in dom g1 and A34: g1 . x1 = g1 . x2 ; ::_thesis: x1 = x2 reconsider n2 = x2 as Element of NAT by A33; reconsider n1 = x1 as Element of NAT by A32; assume A35: x1 <> x2 ; ::_thesis: contradiction percases ( n1 < n2 or n2 < n1 ) by A35, XXREAL_0:1; suppose n1 < n2 ; ::_thesis: contradiction hence contradiction by A34, SEQM_3:1; ::_thesis: verum end; suppose n2 < n1 ; ::_thesis: contradiction hence contradiction by A34, SEQM_3:1; ::_thesis: verum end; end; end; then A36: rng (g ") = NAT by A21, FUNCT_1:33; A37: rng f = rng g proof thus for y being set st y in rng f holds y in rng g :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: rng g c= rng f proof let y be set ; ::_thesis: ( y in rng f implies y in rng g ) assume A38: y in rng f ; ::_thesis: y in rng g then reconsider y9 = y as Element of NAT by A7; defpred S4[ Element of NAT ] means g1 . $1 < y9; assume A39: not y in rng g ; ::_thesis: contradiction A40: for n being Element of NAT st S4[n] holds S4[n + 1] proof let n be Element of NAT ; ::_thesis: ( S4[n] implies S4[n + 1] ) reconsider m = g . n as Element of NAT by A26; reconsider B = { k where k is Element of NAT : ( k in rng f & k > m ) } as non empty Subset of NAT by A14, A17; A41: ( g . (n + 1) = min B & g . (n + 1) in rng g ) by A21, A23, FUNCT_1:def_3; assume g1 . n < y9 ; ::_thesis: S4[n + 1] then y9 in { k where k is Element of NAT : ( k in rng f & k > m ) } by A38; then A42: min B <= y9 by XXREAL_2:def_7; assume not g1 . (n + 1) < y9 ; ::_thesis: contradiction hence contradiction by A39, A42, A41, XXREAL_0:1; ::_thesis: verum end; A43: S4[ 0 ] proof assume A44: not g1 . 0 < y9 ; ::_thesis: contradiction ( min A <= y9 & g . 0 in rng g ) by A21, A38, FUNCT_1:def_3, XXREAL_2:def_7; hence contradiction by A22, A39, A44, XXREAL_0:1; ::_thesis: verum end; A45: for n being Element of NAT holds S4[n] from NAT_1:sch_1(A43, A40); rng g c= y9 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in y9 ) assume y in rng g ; ::_thesis: y in y9 then consider x being set such that A46: x in dom g and A47: y = g . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A21, A46; g1 . x < y9 by A45; then g1 . x in { i where i is Element of NAT : i < y9 } ; hence y in y9 by A47, AXIOMS:4; ::_thesis: verum end; then rng g is finite ; hence contradiction by A21, A31, CARD_1:59; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng f ) assume y in rng g ; ::_thesis: y in rng f then consider x being set such that A48: x in dom g and A49: y = g . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A21, A48; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: y in rng f hence y in rng f by A22, A49, XXREAL_2:def_7; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: y in rng f then n > 0 by NAT_1:3; then n + 1 > 0 + 1 by XREAL_1:6; then 1 <= n by NAT_1:13; then reconsider m = n - 1 as Element of NAT by INT_1:5; reconsider l = g . m as Element of NAT by A26; reconsider B = { k where k is Element of NAT : ( k in rng f & k > l ) } as non empty Subset of NAT by A14, A17; m + 1 = n ; then g . n = min B by A23; then y in B by A49, XXREAL_2:def_7; then ex k being Element of NAT st ( k = y & k in rng f & k > l ) ; hence y in rng f ; ::_thesis: verum end; end; end; then A50: rng f = dom (g ") by A31, FUNCT_1:33; then ( dom ((g ") * f) = dom f & rng ((g ") * f) = rng (g ") ) by RELAT_1:27, RELAT_1:28; then reconsider P = (g ") * f as Function of NAT,NAT by A6, A36, FUNCT_2:def_1, RELSET_1:4; rng (g ") = dom g by A31, FUNCT_1:33; then rng P = NAT by A21, A50, RELAT_1:28; then P is onto by FUNCT_2:def_3; then reconsider P = P as Permutation of NAT by A9, A31; take P " ; ::_thesis: S2 * (P ") is subsequence of S1 ( NAT = dom (S2 * (P ")) & NAT = dom (S1 * g) & ( for x being set st x in NAT holds (S2 * (P ")) . x = (S1 * g) . x ) ) proof thus NAT = dom (S2 * (P ")) by FUNCT_2:def_1; ::_thesis: ( NAT = dom (S1 * g) & ( for x being set st x in NAT holds (S2 * (P ")) . x = (S1 * g) . x ) ) rng g c= dom S1 by A28, NORMSP_1:12; hence NAT = dom (S1 * g) by A21, RELAT_1:27; ::_thesis: for x being set st x in NAT holds (S2 * (P ")) . x = (S1 * g) . x let x be set ; ::_thesis: ( x in NAT implies (S2 * (P ")) . x = (S1 * g) . x ) assume A51: x in NAT ; ::_thesis: (S2 * (P ")) . x = (S1 * g) . x then A52: g . x in rng g by A21, FUNCT_1:def_3; then A53: (f ") . (g . x) in dom f by A9, A37, FUNCT_1:32; dom (P ") = NAT by FUNCT_2:def_1; hence (S2 * (P ")) . x = S2 . ((((g ") * f) ") . x) by A51, FUNCT_1:13 .= S2 . (((f ") * ((g ") ")) . x) by A9, A31, FUNCT_1:44 .= S2 . (((f ") * g) . x) by A31, FUNCT_1:43 .= S2 . ((f ") . (g . x)) by A21, A51, FUNCT_1:13 .= S1 . (f . ((f ") . (g . x))) by A6, A8, A53 .= S1 . (g . x) by A9, A37, A52, FUNCT_1:35 .= (S1 * g) . x by A21, A51, FUNCT_1:13 ; ::_thesis: verum end; then S2 * (P ") = S1 * g1 by FUNCT_1:2; hence S2 * (P ") is subsequence of S1 ; ::_thesis: verum end; scheme :: FRECHET2:sch 1 PermSeq{ F1() -> non empty 1-sorted , F2() -> sequence of F1(), F3() -> Permutation of NAT, P1[ set ] } : ex n being Element of NAT st for m being Element of NAT st n <= m holds P1[(F2() * F3()) . m] provided A1: ex n being Element of NAT st for m being Element of NAT for x being Point of F1() st n <= m & x = F2() . m holds P1[x] proof consider n being Element of NAT such that A2: for m being Element of NAT for x being Point of F1() st n <= m & x = F2() . m holds P1[x] by A1; ( n in succ n & dom (F3() ") = NAT ) by FUNCT_2:def_1, ORDINAL1:6; then (F3() ") . n in (F3() ") .: (succ n) by FUNCT_1:def_6; then reconsider X = (F3() ") .: (succ n) as non empty finite Subset of NAT ; reconsider mX = (max X) + 1 as Element of NAT ; take mX ; ::_thesis: for m being Element of NAT st mX <= m holds P1[(F2() * F3()) . m] let m be Element of NAT ; ::_thesis: ( mX <= m implies P1[(F2() * F3()) . m] ) m in NAT ; then A3: m in dom F3() by FUNCT_2:52; assume A4: mX <= m ; ::_thesis: P1[(F2() * F3()) . m] n <= F3() . m proof assume F3() . m < n ; ::_thesis: contradiction then F3() . m in { p1 where p1 is Element of NAT : p1 < n } ; then F3() . m in n by AXIOMS:4; then F3() . m in succ n by ORDINAL1:8; then m in F3() " (succ n) by A3, FUNCT_1:def_7; then m in (F3() ") .: (succ n) by FUNCT_1:85; then m <= max X by XXREAL_2:def_8; hence contradiction by A4, NAT_1:13; ::_thesis: verum end; then A5: P1[F2() . (F3() . m)] by A2; m in NAT ; then m in dom F3() by FUNCT_2:def_1; hence P1[(F2() * F3()) . m] by A5, FUNCT_1:13; ::_thesis: verum end; scheme :: FRECHET2:sch 2 PermSeq2{ F1() -> non empty TopStruct , F2() -> sequence of F1(), F3() -> Permutation of NAT, P1[ set ] } : ex n being Element of NAT st for m being Element of NAT st n <= m holds P1[(F2() * F3()) . m] provided A1: ex n being Element of NAT st for m being Element of NAT for x being Point of F1() st n <= m & x = F2() . m holds P1[x] proof reconsider T1 = F1() as non empty 1-sorted ; reconsider S1 = F2() as sequence of T1 ; A2: ex n being Element of NAT st for m being Element of NAT for x being Point of T1 st n <= m & x = S1 . m holds P1[x] by A1; ex n being Element of NAT st for m being Element of NAT st n <= m holds P1[(S1 * F3()) . m] from FRECHET2:sch_1(A2); hence ex n being Element of NAT st for m being Element of NAT st n <= m holds P1[(F2() * F3()) . m] ; ::_thesis: verum end; theorem Th37: :: FRECHET2:37 for T being non empty TopStruct for S being sequence of T for P being Permutation of NAT for x being Point of T st S is_convergent_to x holds S * P is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for P being Permutation of NAT for x being Point of T st S is_convergent_to x holds S * P is_convergent_to x let S be sequence of T; ::_thesis: for P being Permutation of NAT for x being Point of T st S is_convergent_to x holds S * P is_convergent_to x let P be Permutation of NAT; ::_thesis: for x being Point of T st S is_convergent_to x holds S * P is_convergent_to x let x be Point of T; ::_thesis: ( S is_convergent_to x implies S * P is_convergent_to x ) assume A1: S is_convergent_to x ; ::_thesis: S * P is_convergent_to x for U1 being Subset of T st U1 is open & x in U1 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds (S * P) . m in U1 proof let U1 be Subset of T; ::_thesis: ( U1 is open & x in U1 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds (S * P) . m in U1 ) defpred S1[ set ] means $1 in U1; assume A2: ( U1 is open & x in U1 ) ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds (S * P) . m in U1 A3: ex n being Element of NAT st for m being Element of NAT for x being Point of T st n <= m & x = S . m holds S1[x] proof consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds S . m in U1 by A1, A2, FRECHET:def_3; take n ; ::_thesis: for m being Element of NAT for x being Point of T st n <= m & x = S . m holds S1[x] let m be Element of NAT ; ::_thesis: for x being Point of T st n <= m & x = S . m holds S1[x] let x be Point of T; ::_thesis: ( n <= m & x = S . m implies S1[x] ) assume ( n <= m & x = S . m ) ; ::_thesis: S1[x] hence S1[x] by A4; ::_thesis: verum end; thus ex n being Element of NAT st for m being Element of NAT st n <= m holds S1[(S * P) . m] from FRECHET2:sch_2(A3); ::_thesis: verum end; hence S * P is_convergent_to x by FRECHET:def_3; ::_thesis: verum end; theorem :: FRECHET2:38 for n0 being Element of NAT ex NS being increasing sequence of NAT st for n being Element of NAT holds NS . n = n + n0 proof let n0 be Element of NAT ; ::_thesis: ex NS being increasing sequence of NAT st for n being Element of NAT holds NS . n = n + n0 deffunc H1( Element of NAT ) -> Element of NAT = $1 + n0; consider NS being Real_Sequence such that A1: for n being Element of NAT holds NS . n = H1(n) from SEQ_1:sch_1(); A2: NS is increasing proof let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: not NS . (n + 1) <= NS . n n < n + 1 by NAT_1:13; then n + n0 < (n + 1) + n0 by XREAL_1:6; then NS . n < (n + 1) + n0 by A1; hence not NS . (n + 1) <= NS . n by A1; ::_thesis: verum end; for n being Element of NAT holds NS . n is Element of NAT proof let n be Element of NAT ; ::_thesis: NS . n is Element of NAT n + n0 in NAT ; hence NS . n is Element of NAT by A1; ::_thesis: verum end; then reconsider NS = NS as increasing sequence of NAT by A2, SEQM_3:13; take NS ; ::_thesis: for n being Element of NAT holds NS . n = n + n0 thus for n being Element of NAT holds NS . n = n + n0 by A1; ::_thesis: verum end; theorem Th39: :: FRECHET2:39 for T being non empty TopStruct for S being sequence of T for x being Point of T for n0 being Nat st x is_a_cluster_point_of S holds x is_a_cluster_point_of S ^\ n0 proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T for n0 being Nat st x is_a_cluster_point_of S holds x is_a_cluster_point_of S ^\ n0 let S be sequence of T; ::_thesis: for x being Point of T for n0 being Nat st x is_a_cluster_point_of S holds x is_a_cluster_point_of S ^\ n0 let x be Point of T; ::_thesis: for n0 being Nat st x is_a_cluster_point_of S holds x is_a_cluster_point_of S ^\ n0 let n0 be Nat; ::_thesis: ( x is_a_cluster_point_of S implies x is_a_cluster_point_of S ^\ n0 ) assume A1: x is_a_cluster_point_of S ; ::_thesis: x is_a_cluster_point_of S ^\ n0 set S1 = S ^\ n0; let O be Subset of T; :: according to FRECHET2:def_3 ::_thesis: for n being Element of NAT st O is open & x in O holds ex m being Element of NAT st ( n <= m & (S ^\ n0) . m in O ) let n be Element of NAT ; ::_thesis: ( O is open & x in O implies ex m being Element of NAT st ( n <= m & (S ^\ n0) . m in O ) ) assume ( O is open & x in O ) ; ::_thesis: ex m being Element of NAT st ( n <= m & (S ^\ n0) . m in O ) then consider m0 being Element of NAT such that A2: n + n0 <= m0 and A3: S . m0 in O by A1, Def3; ( n0 in NAT & n0 <= n + n0 ) by NAT_1:11, ORDINAL1:def_12; then reconsider m = m0 - n0 as Element of NAT by A2, INT_1:5, XXREAL_0:2; take m ; ::_thesis: ( n <= m & (S ^\ n0) . m in O ) thus n <= m by A2, XREAL_1:19; ::_thesis: (S ^\ n0) . m in O (S ^\ n0) . m = S . ((m0 - n0) + n0) by NAT_1:def_3 .= S . m0 ; hence (S ^\ n0) . m in O by A3; ::_thesis: verum end; theorem Th40: :: FRECHET2:40 for T being non empty TopStruct for S being sequence of T for x being Point of T st x is_a_cluster_point_of S holds x in Cl (rng S) proof let T be non empty TopStruct ; ::_thesis: for S being sequence of T for x being Point of T st x is_a_cluster_point_of S holds x in Cl (rng S) let S be sequence of T; ::_thesis: for x being Point of T st x is_a_cluster_point_of S holds x in Cl (rng S) let x be Point of T; ::_thesis: ( x is_a_cluster_point_of S implies x in Cl (rng S) ) assume A1: x is_a_cluster_point_of S ; ::_thesis: x in Cl (rng S) for G being Subset of T st G is open & x in G holds rng S meets G proof let G be Subset of T; ::_thesis: ( G is open & x in G implies rng S meets G ) assume A2: G is open ; ::_thesis: ( not x in G or rng S meets G ) assume x in G ; ::_thesis: rng S meets G then consider m being Element of NAT such that 0 <= m and A3: S . m in G by A1, A2, Def3; m in NAT ; then m in dom S by NORMSP_1:12; then S . m in rng S by FUNCT_1:def_3; then S . m in (rng S) /\ G by A3, XBOOLE_0:def_4; hence rng S meets G by XBOOLE_0:def_7; ::_thesis: verum end; hence x in Cl (rng S) by PRE_TOPC:def_7; ::_thesis: verum end; theorem :: FRECHET2:41 for T being non empty TopStruct st T is Frechet holds for S being sequence of T for x being Point of T st x is_a_cluster_point_of S holds ex S1 being subsequence of S st S1 is_convergent_to x proof let T be non empty TopStruct ; ::_thesis: ( T is Frechet implies for S being sequence of T for x being Point of T st x is_a_cluster_point_of S holds ex S1 being subsequence of S st S1 is_convergent_to x ) assume A1: T is Frechet ; ::_thesis: for S being sequence of T for x being Point of T st x is_a_cluster_point_of S holds ex S1 being subsequence of S st S1 is_convergent_to x let S be sequence of T; ::_thesis: for x being Point of T st x is_a_cluster_point_of S holds ex S1 being subsequence of S st S1 is_convergent_to x let x be Point of T; ::_thesis: ( x is_a_cluster_point_of S implies ex S1 being subsequence of S st S1 is_convergent_to x ) assume A2: x is_a_cluster_point_of S ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x defpred S1[ Point of T] means x in Cl {$1}; reconsider Y = { y where y is Point of T : S1[y] } as Subset of T from DOMAIN_1:sch_7(); percases ( for n being Element of NAT ex m being Element of NAT st ( m >= n & S . m in Y ) or ex n being Element of NAT st for m being Element of NAT st m >= n holds not S . m in Y ) ; supposeA3: for n being Element of NAT ex m being Element of NAT st ( m >= n & S . m in Y ) ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x defpred S2[ set ] means $1 in Y; A4: for n being Element of NAT ex m being Element of NAT st ( n <= m & S2[S . m] ) by A3; consider S1 being subsequence of S such that A5: for n being Element of NAT holds S2[S1 . n] from VALUED_1:sch_1(A4); take S1 ; ::_thesis: S1 is_convergent_to x rng S1 c= Y proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng S1 or y in Y ) assume y in rng S1 ; ::_thesis: y in Y then consider n being set such that A6: n in dom S1 and A7: y = S1 . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; S1 . n in Y by A5; hence y in Y by A7; ::_thesis: verum end; hence S1 is_convergent_to x by Th33; ::_thesis: verum end; suppose ex n being Element of NAT st for m being Element of NAT st m >= n holds not S . m in Y ; ::_thesis: ex S1 being subsequence of S st S1 is_convergent_to x then consider n0 being Element of NAT such that A8: for m being Element of NAT st m >= n0 holds not S . m in Y ; set S9 = S ^\ n0; x in Cl (rng (S ^\ n0)) by A2, Th39, Th40; then consider S2 being sequence of T such that A9: rng S2 c= rng (S ^\ n0) and A10: x in Lim S2 by A1, FRECHET:def_6; A11: S2 is_convergent_to x by A10, FRECHET:def_5; A12: for n being Element of NAT holds not (S ^\ n0) . n in Y proof let n be Element of NAT ; ::_thesis: not (S ^\ n0) . n in Y not S . (n + n0) in Y by A8, NAT_1:11; hence not (S ^\ n0) . n in Y by NAT_1:def_3; ::_thesis: verum end; (rng (S ^\ n0)) /\ Y = {} proof set y = the Element of (rng (S ^\ n0)) /\ Y; assume A13: (rng (S ^\ n0)) /\ Y <> {} ; ::_thesis: contradiction then the Element of (rng (S ^\ n0)) /\ Y in rng (S ^\ n0) by XBOOLE_0:def_4; then consider n being set such that A14: n in dom (S ^\ n0) and A15: the Element of (rng (S ^\ n0)) /\ Y = (S ^\ n0) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A14; not (S ^\ n0) . n in Y by A12; hence contradiction by A13, A15, XBOOLE_0:def_4; ::_thesis: verum end; then rng (S ^\ n0) misses Y by XBOOLE_0:def_7; then consider S29 being subsequence of S2 such that A16: S29 is one-to-one by A9, A11, Th35, XBOOLE_1:63; rng S29 c= rng S2 by VALUED_0:21; then consider P being Permutation of NAT such that A17: S29 * P is subsequence of S ^\ n0 by A9, A16, Th36, XBOOLE_1:1; reconsider S1 = S29 * P as subsequence of S ^\ n0 by A17; reconsider S1 = S1 as subsequence of S by VALUED_0:20; take S1 ; ::_thesis: S1 is_convergent_to x S29 is_convergent_to x by A11, Th15; hence S1 is_convergent_to x by Th37; ::_thesis: verum end; end; end; begin theorem :: FRECHET2:42 for T being non empty TopSpace st T is first-countable holds for x being Point of T ex B being Basis of x ex S being Function st ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds S . m c= S . n ) ) by Lm5; theorem :: FRECHET2:43 for T being non empty TopSpace st ( for p being Point of T holds Cl {p} = {p} ) holds T is T_1 by Lm1; theorem :: FRECHET2:44 for T being non empty TopSpace st T is T_2 holds T is T_1 by Lm4; theorem :: FRECHET2:45 for T being non empty TopSpace st not T is T_1 holds ex x1, x2 being Point of T ex S being sequence of T st ( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) by Lm3;