reconsider n = n as Element of NAT by ORDINAL1:def 12;
set g = incl (f,n);

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

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;

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 )

proof

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;

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

end;

end;