let n be Element of NAT ; :: thesis: for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
let f be Function of (TOP-REAL n),R^1 ; :: thesis: for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
let i be Element of NAT ; :: thesis: ( i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) implies f is continuous )
assume that
A1: i in Seg n and
A2: for p being Element of (TOP-REAL n) holds f . p = p /. i ; :: thesis: f is continuous
reconsider f1 = f as Function of (TOP-REAL n),(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
for r being real number
for u being Element of RealSpace
for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is open

proof

let r be real number ; :: thesis: for u being Element of RealSpace
for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is open
let u be Element of RealSpace ; :: thesis: for P being Subset of (TopSpaceMetr RealSpace ) st r > 0 & P = Ball u,r holds
f1 " P is open
let P be Subset of (TopSpaceMetr RealSpace ); :: thesis: ( r > 0 & P = Ball u,r implies f1 " P is open )
assume that
r > 0 and
A3: P = Ball u,r ; :: thesis: f1 " P is open
reconsider u1 = u as Real by METRIC_1:def 14;
Ball u,r = { s where s is Real : ( u1 - r < s & s < u1 + r ) } by Th21;
then f " (Ball u,r) = { p where p is Element of (TOP-REAL n) : ( u1 - r < p /. i & p /. i < u1 + r ) } by A2, Th19;
hence f1 " P is open by A1, A3, Th18; :: thesis: verum

end;

hence f is continuous by Th20, TOPMETR:def 7; :: thesis: verum