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 () ;
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 () 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 () 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 (); :: 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 ;
reconsider s = (incl (f,n)) . p as Point of () by EUCLID:67;
consider r being Real such that
A6: r > 0 and
A7: Ball (s,r) c= V by ;
reconsider G = n |-> (f . p) as FinSequence of REAL ;
1 <= n by ;
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
.= f . p by ;
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 ;
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 (); :: 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 () by EUCLID:67;
reconsider y2 = y1, s2 = s as Element of REAL n ;
A16: y2 = n |-> (f . x) by ;
A17: () . (y1,s) = |.(y2 - s2).| by EUCLID:def 6
.= (sqrt n) * |.((f . x) - (f . p)).| by ;
f . x in f .: W by ;
then |.((f . x) - (f . p)).| < r / (sqrt n) by ;
then dist (y1,s) < r by ;
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;