let A be Subset of REAL?; :: according to FRECHET:def 6 :: thesis: for x being Point of REAL? st x in Cl A holds

ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

let x be Point of REAL?; :: thesis: ( x in Cl A implies ex S being sequence of REAL? st

( rng S c= A & x in Lim S ) )

assume A1: x in Cl A ; :: thesis: ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

x in the carrier of REAL? ;

then x in (REAL \ NAT) \/ {REAL} by Def8;

then A2: ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def 3;

ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

let x be Point of REAL?; :: thesis: ( x in Cl A implies ex S being sequence of REAL? st

( rng S c= A & x in Lim S ) )

assume A1: x in Cl A ; :: thesis: ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

x in the carrier of REAL? ;

then x in (REAL \ NAT) \/ {REAL} by Def8;

then A2: ( x in REAL \ NAT or x in {REAL} ) by XBOOLE_0:def 3;

per cases
( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) )
by A2, TARSKI:def 1;

end;

suppose A3:
x in REAL \ NAT
; :: thesis: ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

( rng S c= A & x in Lim S )

then A4:
x in REAL
;

A c= the carrier of REAL? ;

then A5: A c= (REAL \ NAT) \/ {REAL} by Def8;

A \ {REAL} c= REAL

reconsider x9 = x as Point of R^1 by A3, TOPMETR:17;

reconsider A9 = A9 as Subset of R^1 ;

for B9 being Subset of R^1 st B9 is open & x9 in B9 holds

A9 meets B9

then consider S9 being sequence of R^1 such that

A15: rng S9 c= A9 and

A16: x9 in Lim S9 by Def6;

A17: rng S9 c= A by A15, XBOOLE_0:def 5;

then reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1:1;

take S ; :: thesis: ( rng S c= A & x in Lim S )

thus rng S c= A by A17; :: thesis: x in Lim S

A18: S9 is_convergent_to x9 by A16, Def5;

S is_convergent_to x

end;A c= the carrier of REAL? ;

then A5: A c= (REAL \ NAT) \/ {REAL} by Def8;

A \ {REAL} c= REAL

proof

then reconsider A9 = A \ {REAL} as Subset of R^1 by TOPMETR:17;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A \ {REAL} or a in REAL )

assume A6: a in A \ {REAL} ; :: thesis: a in REAL

then a in A by XBOOLE_0:def 5;

then ( a in REAL \ NAT or a in {REAL} ) by A5, XBOOLE_0:def 3;

hence a in REAL by A6, XBOOLE_0:def 5; :: thesis: verum

end;assume A6: a in A \ {REAL} ; :: thesis: a in REAL

then a in A by XBOOLE_0:def 5;

then ( a in REAL \ NAT or a in {REAL} ) by A5, XBOOLE_0:def 3;

hence a in REAL by A6, XBOOLE_0:def 5; :: thesis: verum

reconsider x9 = x as Point of R^1 by A3, TOPMETR:17;

reconsider A9 = A9 as Subset of R^1 ;

for B9 being Subset of R^1 st B9 is open & x9 in B9 holds

A9 meets B9

proof

then
x9 in Cl A9
by PRE_TOPC:def 7;
reconsider C = NAT as Subset of R^1 by TOPMETR:17, NUMBERS:19;

let B9 be Subset of R^1; :: thesis: ( B9 is open & x9 in B9 implies A9 meets B9 )

reconsider B1 = B9 as Subset of R^1 ;

reconsider C = C as Subset of R^1 ;

A7: not x9 in NAT by A3, XBOOLE_0:def 5;

B9 \ NAT misses NAT by XBOOLE_1:79;

then A8: (B9 \ NAT) /\ NAT = {} ;

then reconsider D = B1 \ C as Subset of REAL? by Th29;

assume B9 is open ; :: thesis: ( not x9 in B9 or A9 meets B9 )

then B1 \ C is open by Th4, Th10;

then A9: D is open by A8, Th30;

reconsider D = D as Subset of REAL? ;

assume x9 in B9 ; :: thesis: A9 meets B9

then x9 in B9 \ NAT by A7, XBOOLE_0:def 5;

then A meets D by A1, A9, PRE_TOPC:def 7;

then A10: A /\ D <> {} ;

A9 /\ B9 <> {}

end;let B9 be Subset of R^1; :: thesis: ( B9 is open & x9 in B9 implies A9 meets B9 )

reconsider B1 = B9 as Subset of R^1 ;

reconsider C = C as Subset of R^1 ;

A7: not x9 in NAT by A3, XBOOLE_0:def 5;

B9 \ NAT misses NAT by XBOOLE_1:79;

then A8: (B9 \ NAT) /\ NAT = {} ;

then reconsider D = B1 \ C as Subset of REAL? by Th29;

assume B9 is open ; :: thesis: ( not x9 in B9 or A9 meets B9 )

then B1 \ C is open by Th4, Th10;

then A9: D is open by A8, Th30;

reconsider D = D as Subset of REAL? ;

assume x9 in B9 ; :: thesis: A9 meets B9

then x9 in B9 \ NAT by A7, XBOOLE_0:def 5;

then A meets D by A1, A9, PRE_TOPC:def 7;

then A10: A /\ D <> {} ;

A9 /\ B9 <> {}

proof

hence
A9 meets B9
; :: thesis: verum
set a = the Element of A /\ D;

A11: the Element of A /\ D in D by A10, XBOOLE_0:def 4;

then A12: the Element of A /\ D in B9 by XBOOLE_0:def 5;

A13: the Element of A /\ D in REAL by A11, TOPMETR:17;

A14: not the Element of A /\ D in {REAL}

then the Element of A /\ D in A \ {REAL} by A14, XBOOLE_0:def 5;

hence A9 /\ B9 <> {} by A12, XBOOLE_0:def 4; :: thesis: verum

end;A11: the Element of A /\ D in D by A10, XBOOLE_0:def 4;

then A12: the Element of A /\ D in B9 by XBOOLE_0:def 5;

A13: the Element of A /\ D in REAL by A11, TOPMETR:17;

A14: not the Element of A /\ D in {REAL}

proof

the Element of A /\ D in A
by A10, XBOOLE_0:def 4;
assume
the Element of A /\ D in {REAL}
; :: thesis: contradiction

then the Element of A /\ D = REAL by TARSKI:def 1;

hence contradiction by A13; :: thesis: verum

end;then the Element of A /\ D = REAL by TARSKI:def 1;

hence contradiction by A13; :: thesis: verum

then the Element of A /\ D in A \ {REAL} by A14, XBOOLE_0:def 5;

hence A9 /\ B9 <> {} by A12, XBOOLE_0:def 4; :: thesis: verum

then consider S9 being sequence of R^1 such that

A15: rng S9 c= A9 and

A16: x9 in Lim S9 by Def6;

A17: rng S9 c= A by A15, XBOOLE_0:def 5;

then reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1:1;

take S ; :: thesis: ( rng S c= A & x in Lim S )

thus rng S c= A by A17; :: thesis: x in Lim S

A18: S9 is_convergent_to x9 by A16, Def5;

S is_convergent_to x

proof

hence
x in Lim S
by Def5; :: thesis: verum
reconsider C = {REAL} as Subset of REAL? by Lm3;

let V be Subset of REAL?; :: according to FRECHET:def 3 :: thesis: ( V is open & x in V implies ex n being Nat st

for m being Nat st n <= m holds

S . m in V )

assume that

A19: V is open and

A20: x in V ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in V

reconsider C = C as Subset of REAL? ;

REAL in {REAL} by TARSKI:def 1;

then A21: not REAL in V \ {REAL} by XBOOLE_0:def 5;

then reconsider V9 = V \ C as Subset of R^1 by Th29;

V \ C is open by A19, Th4, Th31;

then A22: V9 is open by A21, Th30;

not x in C

then consider n being Nat such that

A23: for m being Nat st n <= m holds

S9 . m in V9 by A18, A22;

take n ; :: thesis: for m being Nat st n <= m holds

S . m in V

let m be Nat; :: thesis: ( n <= m implies S . m in V )

assume n <= m ; :: thesis: S . m in V

then S9 . m in V9 by A23;

hence S . m in V by XBOOLE_0:def 5; :: thesis: verum

end;let V be Subset of REAL?; :: according to FRECHET:def 3 :: thesis: ( V is open & x in V implies ex n being Nat st

for m being Nat st n <= m holds

S . m in V )

assume that

A19: V is open and

A20: x in V ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in V

reconsider C = C as Subset of REAL? ;

REAL in {REAL} by TARSKI:def 1;

then A21: not REAL in V \ {REAL} by XBOOLE_0:def 5;

then reconsider V9 = V \ C as Subset of R^1 by Th29;

V \ C is open by A19, Th4, Th31;

then A22: V9 is open by A21, Th30;

not x in C

proof

then
x in V \ C
by A20, XBOOLE_0:def 5;
assume
x in C
; :: thesis: contradiction

then x = REAL by TARSKI:def 1;

hence contradiction by A4; :: thesis: verum

end;then x = REAL by TARSKI:def 1;

hence contradiction by A4; :: thesis: verum

then consider n being Nat such that

A23: for m being Nat st n <= m holds

S9 . m in V9 by A18, A22;

take n ; :: thesis: for m being Nat st n <= m holds

S . m in V

let m be Nat; :: thesis: ( n <= m implies S . m in V )

assume n <= m ; :: thesis: S . m in V

then S9 . m in V9 by A23;

hence S . m in V by XBOOLE_0:def 5; :: thesis: verum

suppose A24:
( x = REAL & x in A )
; :: thesis: ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

( rng S c= A & x in Lim S )

reconsider S = NAT --> x as sequence of REAL? ;

take S ; :: thesis: ( rng S c= A & x in Lim S )

{x} c= A by A24, ZFMISC_1:31;

hence rng S c= A by FUNCOP_1:8; :: thesis: x in Lim S

S is_convergent_to x by Th22;

hence x in Lim S by Def5; :: thesis: verum

end;take S ; :: thesis: ( rng S c= A & x in Lim S )

{x} c= A by A24, ZFMISC_1:31;

hence rng S c= A by FUNCOP_1:8; :: thesis: x in Lim S

S is_convergent_to x by Th22;

hence x in Lim S by Def5; :: thesis: verum

suppose A25:
( x = REAL & not x in A )
; :: thesis: ex S being sequence of REAL? st

( rng S c= A & x in Lim S )

( rng S c= A & x in Lim S )

then reconsider A9 = A as Subset of R^1 by Th29;

ex k being Point of R^1 st

( k in NAT & ex S9 being sequence of R^1 st

( rng S9 c= A9 & S9 is_convergent_to k ) )

A61: k in NAT and

A62: ex S9 being sequence of R^1 st

( rng S9 c= A9 & S9 is_convergent_to k ) ;

consider S9 being sequence of R^1 such that

A63: rng S9 c= A9 and

A64: S9 is_convergent_to k by A62;

reconsider S = S9 as sequence of REAL? by A63, Th2, XBOOLE_1:1;

take S ; :: thesis: ( rng S c= A & x in Lim S )

thus rng S c= A by A63; :: thesis: x in Lim S

S is_convergent_to x

end;ex k being Point of R^1 st

( k in NAT & ex S9 being sequence of R^1 st

( rng S9 c= A9 & S9 is_convergent_to k ) )

proof

then consider k being Point of R^1 such that
defpred S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & $1 in D2 & $2 in the topology of R^1 & D2 /\ A9 = {} );

assume A26: for k being Point of R^1 holds

( not k in NAT or for S9 being sequence of R^1 holds

( not rng S9 c= A9 or not S9 is_convergent_to k ) ) ; :: thesis: contradiction

A27: for k being object st k in NAT holds

ex U1 being object st S_{1}[k,U1]

A46: ( dom g = NAT & ( for k being object st k in NAT holds

S_{1}[k,g . k] ) )
from CLASSES1:sch 1(A27);

rng g c= bool the carrier of R^1

F is open

(union F) \ NAT c= REAL \ NAT by TOPMETR:17, XBOOLE_1:33;

then ((union F) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9;

then reconsider B = ((union F) \ NAT) \/ {REAL} as Subset of REAL? by Def8;

reconsider B = B as Subset of REAL? ;

A52: B /\ A = {}

then A meets B by A1, A25, PRE_TOPC:def 7;

hence contradiction by A52; :: thesis: verum

end;( D2 = $2 & $1 in D2 & $2 in the topology of R^1 & D2 /\ A9 = {} );

assume A26: for k being Point of R^1 holds

( not k in NAT or for S9 being sequence of R^1 holds

( not rng S9 c= A9 or not S9 is_convergent_to k ) ) ; :: thesis: contradiction

A27: for k being object st k in NAT holds

ex U1 being object st S

proof

consider g being Function such that
given k being object such that A28:
k in NAT
and

A29: for U1 being object holds not S_{1}[k,U1]
; :: thesis: contradiction

reconsider k = k as Point of R^1 by A28, TOPMETR:17, NUMBERS:19;

reconsider k99 = k as Point of (TopSpaceMetr RealSpace) ;

reconsider k9 = k99 as Point of RealSpace by TOPMETR:12;

set Bs = Balls k99;

consider h being sequence of (Balls k99) such that

A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11;

defpred S_{2}[ object , object ] means $2 in (h . $1) /\ A9;

A31: for n being object st n in NAT holds

ex z being object st

( z in the carrier of R^1 & S_{2}[n,z] )

A34: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and

A35: for n being object st n in NAT holds

S_{2}[n,S9 . n]
from FUNCT_1:sch 6(A31);

reconsider S9 = S9 as sequence of the carrier of R^1 by A34, FUNCT_2:2;

A36: S9 is_convergent_to k

end;A29: for U1 being object holds not S

reconsider k = k as Point of R^1 by A28, TOPMETR:17, NUMBERS:19;

reconsider k99 = k as Point of (TopSpaceMetr RealSpace) ;

reconsider k9 = k99 as Point of RealSpace by TOPMETR:12;

set Bs = Balls k99;

consider h being sequence of (Balls k99) such that

A30: for n being Element of NAT holds h . n = Ball (k9,(1 / (n + 1))) by Th11;

defpred S

A31: for n being object st n in NAT holds

ex z being object st

( z in the carrier of R^1 & S

proof

consider S9 being Function such that
let n be object ; :: thesis: ( n in NAT implies ex z being object st

( z in the carrier of R^1 & S_{2}[n,z] ) )

assume n in NAT ; :: thesis: ex z being object st

( z in the carrier of R^1 & S_{2}[n,z] )

then reconsider n = n as Element of NAT ;

A32: h . n in Balls k99 ;

then reconsider H = h . n as Subset of R^1 ;

take z = the Element of H /\ A9; :: thesis: ( z in the carrier of R^1 & S_{2}[n,z] )

Balls k99 c= the topology of R^1 by TOPS_2:64;

then A33: H /\ A9 <> {} by A29, A32, YELLOW_8:12;

then z in H by XBOOLE_0:def 4;

hence ( z in the carrier of R^1 & S_{2}[n,z] )
by A33; :: thesis: verum

end;( z in the carrier of R^1 & S

assume n in NAT ; :: thesis: ex z being object st

( z in the carrier of R^1 & S

then reconsider n = n as Element of NAT ;

A32: h . n in Balls k99 ;

then reconsider H = h . n as Subset of R^1 ;

take z = the Element of H /\ A9; :: thesis: ( z in the carrier of R^1 & S

Balls k99 c= the topology of R^1 by TOPS_2:64;

then A33: H /\ A9 <> {} by A29, A32, YELLOW_8:12;

then z in H by XBOOLE_0:def 4;

hence ( z in the carrier of R^1 & S

A34: ( dom S9 = NAT & rng S9 c= the carrier of R^1 ) and

A35: for n being object st n in NAT holds

S

reconsider S9 = S9 as sequence of the carrier of R^1 by A34, FUNCT_2:2;

A36: S9 is_convergent_to k

proof

rng S9 c= A9
let U1 be Subset of R^1; :: according to FRECHET:def 3 :: thesis: ( U1 is open & k in U1 implies ex n being Nat st

for m being Nat st n <= m holds

S9 . m in U1 )

assume ( U1 is open & k in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S9 . m in U1

then consider r being Real such that

A37: r > 0 and

A38: Ball (k9,r) c= U1 by TOPMETR:15;

reconsider r = r as Real ;

consider n being Nat such that

A39: 1 / n < r and

A40: n > 0 by A37, Lm1;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: for m being Nat st n <= m holds

S9 . m in U1

let m be Nat; :: thesis: ( n <= m implies S9 . m in U1 )

A41: m in NAT by ORDINAL1:def 12;

S9 . m in (h . m) /\ A9 by A35, A41;

then A42: S9 . m in h . m by XBOOLE_0:def 4;

assume n <= m ; :: thesis: S9 . m in U1

then n < m + 1 by NAT_1:13;

then 1 / (m + 1) < 1 / n by A40, XREAL_1:88;

then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by A39, PCOMPS_1:1, XXREAL_0:2;

then A43: Ball (k9,(1 / (m + 1))) c= U1 by A38;

h . m = Ball (k9,(1 / (m + 1))) by A30, A41;

hence S9 . m in U1 by A43, A42; :: thesis: verum

end;for m being Nat st n <= m holds

S9 . m in U1 )

assume ( U1 is open & k in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S9 . m in U1

then consider r being Real such that

A37: r > 0 and

A38: Ball (k9,r) c= U1 by TOPMETR:15;

reconsider r = r as Real ;

consider n being Nat such that

A39: 1 / n < r and

A40: n > 0 by A37, Lm1;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: for m being Nat st n <= m holds

S9 . m in U1

let m be Nat; :: thesis: ( n <= m implies S9 . m in U1 )

A41: m in NAT by ORDINAL1:def 12;

S9 . m in (h . m) /\ A9 by A35, A41;

then A42: S9 . m in h . m by XBOOLE_0:def 4;

assume n <= m ; :: thesis: S9 . m in U1

then n < m + 1 by NAT_1:13;

then 1 / (m + 1) < 1 / n by A40, XREAL_1:88;

then Ball (k9,(1 / (m + 1))) c= Ball (k9,r) by A39, PCOMPS_1:1, XXREAL_0:2;

then A43: Ball (k9,(1 / (m + 1))) c= U1 by A38;

h . m = Ball (k9,(1 / (m + 1))) by A30, A41;

hence S9 . m in U1 by A43, A42; :: thesis: verum

proof

hence
contradiction
by A26, A28, A36; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng S9 or z in A9 )

assume z in rng S9 ; :: thesis: z in A9

then consider z9 being object such that

A44: z9 in dom S9 and

A45: z = S9 . z9 by FUNCT_1:def 3;

S9 . z9 in (h . z9) /\ A9 by A35, A44;

hence z in A9 by A45, XBOOLE_0:def 4; :: thesis: verum

end;assume z in rng S9 ; :: thesis: z in A9

then consider z9 being object such that

A44: z9 in dom S9 and

A45: z = S9 . z9 by FUNCT_1:def 3;

S9 . z9 in (h . z9) /\ A9 by A35, A44;

hence z in A9 by A45, XBOOLE_0:def 4; :: thesis: verum

A46: ( dom g = NAT & ( for k being object st k in NAT holds

S

rng g c= bool the carrier of R^1

proof

then reconsider F = rng g as Subset-Family of R^1 ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in bool the carrier of R^1 )

assume z in rng g ; :: thesis: z in bool the carrier of R^1

then consider k being object such that

A47: k in dom g and

A48: z = g . k by FUNCT_1:def 3;

S_{1}[k,g . k]
by A46, A47;

then g . k in the topology of R^1 ;

hence z in bool the carrier of R^1 by A48; :: thesis: verum

end;assume z in rng g ; :: thesis: z in bool the carrier of R^1

then consider k being object such that

A47: k in dom g and

A48: z = g . k by FUNCT_1:def 3;

S

then g . k in the topology of R^1 ;

hence z in bool the carrier of R^1 by A48; :: thesis: verum

F is open

proof

then A51:
union F is open
by TOPS_2:19;
let O be Subset of R^1; :: according to TOPS_2:def 1 :: thesis: ( not O in F or O is open )

assume O in F ; :: thesis: O is open

then consider k being object such that

A49: k in dom g and

A50: O = g . k by FUNCT_1:def 3;

S_{1}[k,g . k]
by A46, A49;

then g . k in the topology of R^1 ;

hence O is open by A50, PRE_TOPC:def 2; :: thesis: verum

end;assume O in F ; :: thesis: O is open

then consider k being object such that

A49: k in dom g and

A50: O = g . k by FUNCT_1:def 3;

S

then g . k in the topology of R^1 ;

hence O is open by A50, PRE_TOPC:def 2; :: thesis: verum

(union F) \ NAT c= REAL \ NAT by TOPMETR:17, XBOOLE_1:33;

then ((union F) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL} by XBOOLE_1:9;

then reconsider B = ((union F) \ NAT) \/ {REAL} as Subset of REAL? by Def8;

reconsider B = B as Subset of REAL? ;

A52: B /\ A = {}

proof

NAT c= union F
set z = the Element of B /\ A;

assume A53: B /\ A <> {} ; :: thesis: contradiction

then A54: the Element of B /\ A in B by XBOOLE_0:def 4;

A55: the Element of B /\ A in A by A53, XBOOLE_0:def 4;

end;assume A53: B /\ A <> {} ; :: thesis: contradiction

then A54: the Element of B /\ A in B by XBOOLE_0:def 4;

A55: the Element of B /\ A in A by A53, XBOOLE_0:def 4;

per cases
( the Element of B /\ A in (union F) \ NAT or the Element of B /\ A in {REAL} )
by A54, XBOOLE_0:def 3;

end;

suppose
the Element of B /\ A in (union F) \ NAT
; :: thesis: contradiction

then
the Element of B /\ A in union F
by XBOOLE_0:def 5;

then consider C being set such that

A56: the Element of B /\ A in C and

A57: C in F by TARSKI:def 4;

consider l being object such that

A58: l in dom g and

A59: C = g . l by A57, FUNCT_1:def 3;

S_{1}[l,g . l]
by A46, A58;

then (g . l) /\ A = {} ;

hence contradiction by A55, A56, A59, XBOOLE_0:def 4; :: thesis: verum

end;then consider C being set such that

A56: the Element of B /\ A in C and

A57: C in F by TARSKI:def 4;

consider l being object such that

A58: l in dom g and

A59: C = g . l by A57, FUNCT_1:def 3;

S

then (g . l) /\ A = {} ;

hence contradiction by A55, A56, A59, XBOOLE_0:def 4; :: thesis: verum

suppose
the Element of B /\ A in {REAL}
; :: thesis: contradiction

then
the Element of B /\ A = REAL
by TARSKI:def 1;

hence contradiction by A25, A53, XBOOLE_0:def 4; :: thesis: verum

end;hence contradiction by A25, A53, XBOOLE_0:def 4; :: thesis: verum

proof

then
( B is open & REAL in B )
by A51, Th28;
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in NAT or k in union F )

assume A60: k in NAT ; :: thesis: k in union F

then S_{1}[k,g . k]
by A46;

then ( k in g . k & g . k in rng g ) by A46, FUNCT_1:def 3, A60;

hence k in union F by TARSKI:def 4; :: thesis: verum

end;assume A60: k in NAT ; :: thesis: k in union F

then S

then ( k in g . k & g . k in rng g ) by A46, FUNCT_1:def 3, A60;

hence k in union F by TARSKI:def 4; :: thesis: verum

then A meets B by A1, A25, PRE_TOPC:def 7;

hence contradiction by A52; :: thesis: verum

A61: k in NAT and

A62: ex S9 being sequence of R^1 st

( rng S9 c= A9 & S9 is_convergent_to k ) ;

consider S9 being sequence of R^1 such that

A63: rng S9 c= A9 and

A64: S9 is_convergent_to k by A62;

reconsider S = S9 as sequence of REAL? by A63, Th2, XBOOLE_1:1;

take S ; :: thesis: ( rng S c= A & x in Lim S )

thus rng S c= A by A63; :: thesis: x in Lim S

S is_convergent_to x

proof

hence
x in Lim S
by Def5; :: thesis: verum
let U1 be Subset of REAL?; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Nat st

for m being Nat st n <= m holds

S . m in U1 )

assume ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

then consider O being Subset of R^1 such that

A65: ( O is open & NAT c= O ) and

A66: U1 = (O \ NAT) \/ {REAL} by A25, Th28;

consider n being Nat such that

A67: for m being Nat st n <= m holds

S9 . m in O by A61, A64, A65;

take n ; :: thesis: for m being Nat st n <= m holds

S . m in U1

let m be Nat; :: thesis: ( n <= m implies S . m in U1 )

assume n <= m ; :: thesis: S . m in U1

then A68: S9 . m in O by A67;

A69: m in NAT by ORDINAL1:def 12;

then m in dom S9 by NORMSP_1:12;

then S9 . m in rng S9 by FUNCT_1:def 3;

then S9 . m in A9 by A63;

then S9 . m in the carrier of REAL? ;

then S9 . m in (REAL \ NAT) \/ {REAL} by Def8;

then A70: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def 3;

reconsider m = m as Element of NAT by A69;

S9 . m <> REAL

then S9 . m in O \ NAT by A68, XBOOLE_0:def 5;

hence S . m in U1 by A66, XBOOLE_0:def 3; :: thesis: verum

end;for m being Nat st n <= m holds

S . m in U1 )

assume ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

then consider O being Subset of R^1 such that

A65: ( O is open & NAT c= O ) and

A66: U1 = (O \ NAT) \/ {REAL} by A25, Th28;

consider n being Nat such that

A67: for m being Nat st n <= m holds

S9 . m in O by A61, A64, A65;

take n ; :: thesis: for m being Nat st n <= m holds

S . m in U1

let m be Nat; :: thesis: ( n <= m implies S . m in U1 )

assume n <= m ; :: thesis: S . m in U1

then A68: S9 . m in O by A67;

A69: m in NAT by ORDINAL1:def 12;

then m in dom S9 by NORMSP_1:12;

then S9 . m in rng S9 by FUNCT_1:def 3;

then S9 . m in A9 by A63;

then S9 . m in the carrier of REAL? ;

then S9 . m in (REAL \ NAT) \/ {REAL} by Def8;

then A70: ( S9 . m in REAL \ NAT or S9 . m in {REAL} ) by XBOOLE_0:def 3;

reconsider m = m as Element of NAT by A69;

S9 . m <> REAL

proof

then
not S9 . m in NAT
by A70, TARSKI:def 1, XBOOLE_0:def 5;
A71:
S9 . m in REAL
by TOPMETR:17;

assume S9 . m = REAL ; :: thesis: contradiction

hence contradiction by A71; :: thesis: verum

end;assume S9 . m = REAL ; :: thesis: contradiction

hence contradiction by A71; :: thesis: verum

then S9 . m in O \ NAT by A68, XBOOLE_0:def 5;

hence S . m in U1 by A66, XBOOLE_0:def 3; :: thesis: verum