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

set g = incl (f,n);

set g = incl (f,n);

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

end;

suppose A1:
n = 0
; :: thesis: incl (f,n) is continuous

then reconsider z = 0 as Element of (TOP-REAL n) ;

incl (f,0) = T --> z by Th48;

hence incl (f,n) is continuous by A1; :: thesis: verum

end;incl (f,0) = T --> z by Th48;

hence incl (f,n) is continuous by A1; :: thesis: verum

suppose A2:
n > 0
; :: thesis: incl (f,n) is continuous

for p being Point of T

for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

end;for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

proof

hence
incl (f,n) is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of T; :: thesis: for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds

ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

let V be Subset of (TOP-REAL n); :: thesis: ( (incl (f,n)) . p in V & V is open implies ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V ) )

assume that

A3: (incl (f,n)) . p in V and

A4: V is open ; :: thesis: ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

A5: (incl (f,n)) . p in Int V by A3, A4, TOPS_1:23;

reconsider s = (incl (f,n)) . p as Point of (Euclid n) by EUCLID:67;

consider r being Real such that

A6: r > 0 and

A7: Ball (s,r) c= V by A5, GOBOARD6:5;

reconsider G = n |-> (f . p) as FinSequence of REAL ;

1 <= n by A2, NAT_1:14;

then A8: n in Seg n ;

reconsider F = (incl (f,n)) . p as FinSequence of REAL by EUCLID:24;

A9: F = n |-> (f . p) by Def4;

A10: dom (n |-> (f . p)) = Seg n ;

A11: ((incl (f,n)) . p) /. n = G /. n by Def4

.= G . n by A8, A10, PARTFUN1:def 6

.= f . p by A8, FINSEQ_2:57 ;

set R = r / (sqrt n);

set RR = R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[;

f . p in R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by A2, A11, A6, TOPREAL6:15;

then consider W being Subset of T such that

A12: ( p in W & W is open ) and

A13: f .: W c= R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by JGRAPH_2:10;

take W ; :: thesis: ( p in W & W is open & (incl (f,n)) .: W c= V )

thus ( p in W & W is open ) by A12; :: thesis: (incl (f,n)) .: W c= V

let y be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not y in (incl (f,n)) .: W or y in V )

assume y in (incl (f,n)) .: W ; :: thesis: y in V

then consider x being Element of T such that

A14: x in W and

A15: (incl (f,n)) . x = y by FUNCT_2:65;

reconsider y1 = y as Point of (Euclid n) by EUCLID:67;

reconsider y2 = y1, s2 = s as Element of REAL n ;

A16: y2 = n |-> (f . x) by A15, Def4;

A17: (Pitag_dist n) . (y1,s) = |.(y2 - s2).| by EUCLID:def 6

.= (sqrt n) * |.((f . x) - (f . p)).| by A16, A9, Th11 ;

f . x in f .: W by A14, FUNCT_2:35;

then |.((f . x) - (f . p)).| < r / (sqrt n) by A13, A11, RCOMP_1:1;

then dist (y1,s) < r by A2, A17, XREAL_1:79;

then y in Ball (s,r) by METRIC_1:11;

hence y in V by A7; :: thesis: verum

end;ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

let V be Subset of (TOP-REAL n); :: thesis: ( (incl (f,n)) . p in V & V is open implies ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V ) )

assume that

A3: (incl (f,n)) . p in V and

A4: V is open ; :: thesis: ex W being Subset of T st

( p in W & W is open & (incl (f,n)) .: W c= V )

A5: (incl (f,n)) . p in Int V by A3, A4, TOPS_1:23;

reconsider s = (incl (f,n)) . p as Point of (Euclid n) by EUCLID:67;

consider r being Real such that

A6: r > 0 and

A7: Ball (s,r) c= V by A5, GOBOARD6:5;

reconsider G = n |-> (f . p) as FinSequence of REAL ;

1 <= n by A2, NAT_1:14;

then A8: n in Seg n ;

reconsider F = (incl (f,n)) . p as FinSequence of REAL by EUCLID:24;

A9: F = n |-> (f . p) by Def4;

A10: dom (n |-> (f . p)) = Seg n ;

A11: ((incl (f,n)) . p) /. n = G /. n by Def4

.= G . n by A8, A10, PARTFUN1:def 6

.= f . p by A8, FINSEQ_2:57 ;

set R = r / (sqrt n);

set RR = R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[;

f . p in R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by A2, A11, A6, TOPREAL6:15;

then consider W being Subset of T such that

A12: ( p in W & W is open ) and

A13: f .: W c= R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by JGRAPH_2:10;

take W ; :: thesis: ( p in W & W is open & (incl (f,n)) .: W c= V )

thus ( p in W & W is open ) by A12; :: thesis: (incl (f,n)) .: W c= V

let y be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not y in (incl (f,n)) .: W or y in V )

assume y in (incl (f,n)) .: W ; :: thesis: y in V

then consider x being Element of T such that

A14: x in W and

A15: (incl (f,n)) . x = y by FUNCT_2:65;

reconsider y1 = y as Point of (Euclid n) by EUCLID:67;

reconsider y2 = y1, s2 = s as Element of REAL n ;

A16: y2 = n |-> (f . x) by A15, Def4;

A17: (Pitag_dist n) . (y1,s) = |.(y2 - s2).| by EUCLID:def 6

.= (sqrt n) * |.((f . x) - (f . p)).| by A16, A9, Th11 ;

f . x in f .: W by A14, FUNCT_2:35;

then |.((f . x) - (f . p)).| < r / (sqrt n) by A13, A11, RCOMP_1:1;

then dist (y1,s) < r by A2, A17, XREAL_1:79;

then y in Ball (s,r) by METRIC_1:11;

hence y in V by A7; :: thesis: verum