:: TOPS_4 semantic presentation

begin


theorem Th1: :: TOPS_4:1
for A, B, S, T being TopSpace
for f being Function of A,S
for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
proof
let A, B, S, T be TopSpace; ::_thesis: for f being Function of A,S
for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
let f be Function of A,S; ::_thesis: for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
let g be Function of B,T; ::_thesis: ( TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open implies g is open )
assume that
A1: TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) and
A2: TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) and
A3: f = g and
A4: f is open ; ::_thesis: g is open
let b be Subset of B; :: according to T_0TOPSP:def_2 ::_thesis: ( not b is open or g .: b is open )
assume A5: b is open ; ::_thesis: g .: b is open
reconsider a = b as Subset of A by A1;
 a is open by A1, A5, TOPS_3:76;
then  f .: a is open by A4, T_0TOPSP:def_2;
hence  g .: b is open by A2, A3, TOPS_3:76; ::_thesis: verum
end;

theorem :: TOPS_4:2
for m being Nat
for P being Subset of (TOP-REAL m) holds
( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P )
proof
let m be Nat; ::_thesis: for P being Subset of (TOP-REAL m) holds
( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P )
let P be Subset of (TOP-REAL m); ::_thesis: ( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider P1 = P as Subset of (TopSpaceMetr (Euclid m)) ;
A2: m in NAT by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P ) implies P is open )
assume A3: P is open ; ::_thesis: for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P
let p be Point of (TOP-REAL m); ::_thesis: ( p in P implies ex r being real positive number st Ball (p,r) c= P )
assume A4: p in P ; ::_thesis: ex r being real positive number st Ball (p,r) c= P
reconsider e = p as Point of (Euclid m) by EUCLID:67;
 P1 is open by A3, A1, TOPS_3:76;
then consider r being real number  such that
A5: r > 0 and
A6: Ball (e,r) c= P1 by A4, TOPMETR:15;
reconsider r = r as real positive number by A5;
take r = r; ::_thesis: Ball (p,r) c= P
thus  Ball (p,r) c= P by A2, A6, TOPREAL9:13; ::_thesis: verum
end;
assume A7: for p being Point of (TOP-REAL m) st p in P holds
ex r being real positive number st Ball (p,r) c= P ; ::_thesis: P is open
 for p being Point of (Euclid m) st p in P1 holds
ex r being real number st
( r > 0 & Ball (p,r) c= P1 )
proof
let p be Point of (Euclid m); ::_thesis: ( p in P1 implies ex r being real number st
( r > 0 & Ball (p,r) c= P1 ) )
assume A8: p in P1 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= P1 )
reconsider e = p as Point of (TOP-REAL m) by EUCLID:67;
consider r being real positive number  such that
A9: Ball (e,r) c= P1 by A7, A8;
take  r ; ::_thesis: ( r > 0 & Ball (p,r) c= P1 )
thus  ( r > 0 & Ball (p,r) c= P1 ) by A2, A9, TOPREAL9:13; ::_thesis: verum
end;
then  P1 is open by TOPMETR:15;
hence  P is open by A1, TOPS_3:76; ::_thesis: verum
end;

theorem Th3: :: TOPS_4:3
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is open iff for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is open iff for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) )
let f be Function of X,Y; ::_thesis: ( f is open iff for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) )
thus  ( f is open implies for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) ) ::_thesis: ( ( for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V )
let p be Point of X; ::_thesis: for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V )
let V be open Subset of X; ::_thesis: ( p in V implies ex W being open Subset of Y st
( f . p in W & W c= f .: V ) )
assume A2: p in V ; ::_thesis: ex W being open Subset of Y st
( f . p in W & W c= f .: V )
 V is a_neighborhood of p by A2, CONNSP_2:3;
then consider W being open a_neighborhood of f . p such that
A3: W c= f .: V by A1, TOPGRP_1:22;
take  W ; ::_thesis: ( f . p in W & W c= f .: V )
thus  f . p in W by CONNSP_2:4; ::_thesis: W c= f .: V
thus  W c= f .: V by A3; ::_thesis: verum
end;
assume A4: for p being Point of X
for V being open Subset of X st p in V holds
ex W being open Subset of Y st
( f . p in W & W c= f .: V ) ; ::_thesis: f is open
 for p being Point of X
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P
proof
let p be Point of X; ::_thesis: for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P
let P be open a_neighborhood of p; ::_thesis: ex R being a_neighborhood of f . p st R c= f .: P
consider W being open Subset of Y such that
A5: f . p in W and
A6: W c= f .: P by A4, CONNSP_2:4;
 W is a_neighborhood of f . p by A5, CONNSP_2:3;
hence  ex R being a_neighborhood of f . p st R c= f .: P by A6; ::_thesis: verum
end;
hence  f is open by TOPGRP_1:23; ::_thesis: verum
end;

theorem Th4: :: TOPS_4:4
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V )
proof
let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V )
let M be non empty MetrSpace; ::_thesis: for f being Function of T,(TopSpaceMetr M) holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V )
let f be Function of T,(TopSpaceMetr M); ::_thesis: ( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V )
thus  ( f is open implies for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V ) ::_thesis: ( ( for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let p be Point of T; ::_thesis: for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let V be open Subset of T; ::_thesis: for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let q be Point of M; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V )
assume A2: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V )
assume  p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V
then consider W being open Subset of (TopSpaceMetr M) such that
A3: f . p in W and
A4: W c= f .: V by A1, Th3;
 ex r being real number st
( r > 0 & Ball (q,r) c= W ) by A2, A3, TOPMETR:15;
hence  ex r being real positive number st Ball (q,r) c= f .: V by A4, XBOOLE_1:1; ::_thesis: verum
end;
assume A5: for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V ; ::_thesis: f is open
 for p being Point of T
for V being open Subset of T st p in V holds
ex W being open Subset of (TopSpaceMetr M) st
( f . p in W & W c= f .: V )
proof
let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds
ex W being open Subset of (TopSpaceMetr M) st
( f . p in W & W c= f .: V )
let V be open Subset of T; ::_thesis: ( p in V implies ex W being open Subset of (TopSpaceMetr M) st
( f . p in W & W c= f .: V ) )
reconsider q = f . p as Point of M ;
assume  p in V ; ::_thesis: ex W being open Subset of (TopSpaceMetr M) st
( f . p in W & W c= f .: V )
then consider r being real positive number  such that
A6: Ball (q,r) c= f .: V by A5;
reconsider W = Ball (q,r) as open Subset of (TopSpaceMetr M) by TOPMETR:14;
take  W ; ::_thesis: ( f . p in W & W c= f .: V )
thus  f . p in W by GOBOARD6:1; ::_thesis: W c= f .: V
thus  W c= f .: V by A6; ::_thesis: verum
end;
hence  f is open by Th3; ::_thesis: verum
end;

theorem Th5: :: TOPS_4:5
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is open iff for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
proof
let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is open iff for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M),T holds
( f is open iff for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let f be Function of (TopSpaceMetr M),T; ::_thesis: ( f is open iff for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
hereby  ::_thesis: ( ( for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open )
assume A1: f is open ; ::_thesis: for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let p be Point of M; ::_thesis: for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
A2: p in Ball (p,r) by GOBOARD6:1;
reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M) ;
 V is open by TOPMETR:14;
then consider W being open Subset of T such that
A3: ( f . p in W & W c= f .: V ) by A1, A2, Th3;
take W = W; ::_thesis: ( f . p in W & W c= f .: (Ball (p,r)) )
thus  ( f . p in W & W c= f .: (Ball (p,r)) ) by A3; ::_thesis: verum
end;
assume A4: for p being Point of M
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ; ::_thesis: f is open
 for p being Point of (TopSpaceMetr M)
for V being open Subset of (TopSpaceMetr M) st p in V holds
ex W being open Subset of T st
( f . p in W & W c= f .: V )
proof
let p be Point of (TopSpaceMetr M); ::_thesis: for V being open Subset of (TopSpaceMetr M) st p in V holds
ex W being open Subset of T st
( f . p in W & W c= f .: V )
let V be open Subset of (TopSpaceMetr M); ::_thesis: ( p in V implies ex W being open Subset of T st
( f . p in W & W c= f .: V ) )
reconsider q = p as Point of M ;
assume  p in V ; ::_thesis: ex W being open Subset of T st
( f . p in W & W c= f .: V )
then consider r being real number  such that
A5: r > 0 and
A6: Ball (q,r) c= V by TOPMETR:15;
consider W being open Subset of T such that
A7: f . p in W and
A8: W c= f .: (Ball (q,r)) by A4, A5;
take  W ; ::_thesis: ( f . p in W & W c= f .: V )
thus  f . p in W by A7; ::_thesis: W c= f .: V
 f .: (Ball (q,r)) c= f .: V by A6, RELAT_1:123;
hence  W c= f .: V by A8, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is open by Th3; ::_thesis: verum
end;

theorem Th6: :: TOPS_4:6
for M1, M2 being non empty MetrSpace
for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
proof
let M1, M2 be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); ::_thesis: ( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
thus  ( f is open implies for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) ::_thesis: ( ( for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
let p be Point of M1; ::_thesis: for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
let q be Point of M2; ::_thesis: for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
assume A2: q = f . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M1) ;
A3: p in V by GOBOARD6:1;
 V is open by TOPMETR:14;
hence  ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) by A1, A2, A3, Th4; ::_thesis: verum
end;
assume A4: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ; ::_thesis: f is open
 for p being Point of (TopSpaceMetr M1)
for V being open Subset of (TopSpaceMetr M1)
for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
proof
let p be Point of (TopSpaceMetr M1); ::_thesis: for V being open Subset of (TopSpaceMetr M1)
for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let V be open Subset of (TopSpaceMetr M1); ::_thesis: for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let q be Point of M2; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V )
assume A5: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V )
reconsider p1 = p as Point of M1 ;
assume  p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V
then consider r being real number  such that
A6: r > 0 and
A7: Ball (p1,r) c= V by TOPMETR:15;
A8: f .: (Ball (p1,r)) c= f .: V by A7, RELAT_1:123;
 ex s being real positive number st Ball (q,s) c= f .: (Ball (p1,r)) by A4, A5, A6;
hence  ex r being real positive number st Ball (q,r) c= f .: V by A8, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is open by Th4; ::_thesis: verum
end;

theorem :: TOPS_4:7
for m being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V )
proof
let m be Nat; ::_thesis: for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V )
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL m) holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V )
let f be Function of T,(TOP-REAL m); ::_thesis: ( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider f1 = f as Function of T,(TopSpaceMetr (Euclid m)) ;
A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;
A3: m in NAT by ORDINAL1:def_12;
thus  ( f is open implies for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V ) ::_thesis: ( ( for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V ) implies f is open )
proof
assume A4: f is open ; ::_thesis: for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V
let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V
let V be open Subset of T; ::_thesis: ( p in V implies ex r being real positive number st Ball ((f . p),r) c= f .: V )
assume A5: p in V ; ::_thesis: ex r being real positive number st Ball ((f . p),r) c= f .: V
reconsider fp = f . p as Point of (Euclid m) by EUCLID:67;
 f1 is open by A4, A1, A2, Th1;
then consider r being real positive number  such that
A6: Ball (fp,r) c= f1 .: V by A5, Th4;
 Ball ((f . p),r) = Ball (fp,r) by A3, TOPREAL9:13;
hence  ex r being real positive number st Ball ((f . p),r) c= f .: V by A6; ::_thesis: verum
end;
assume A7: for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st Ball ((f . p),r) c= f .: V ; ::_thesis: f is open
 for p being Point of T
for V being open Subset of T
for q being Point of (Euclid m) st q = f1 . p & p in V holds
ex r being real positive number st Ball (q,r) c= f1 .: V
proof
let p be Point of T; ::_thesis: for V being open Subset of T
for q being Point of (Euclid m) st q = f1 . p & p in V holds
ex r being real positive number st Ball (q,r) c= f1 .: V
let V be open Subset of T; ::_thesis: for q being Point of (Euclid m) st q = f1 . p & p in V holds
ex r being real positive number st Ball (q,r) c= f1 .: V
let q be Point of (Euclid m); ::_thesis: ( q = f1 . p & p in V implies ex r being real positive number st Ball (q,r) c= f1 .: V )
assume A8: q = f1 . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f1 .: V )
assume  p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f1 .: V
then consider r being real positive number  such that
A9: Ball ((f . p),r) c= f .: V by A7;
 Ball ((f . p),r) = Ball (q,r) by A3, A8, TOPREAL9:13;
hence  ex r being real positive number st Ball (q,r) c= f1 .: V by A9; ::_thesis: verum
end;
then  f1 is open by Th4;
hence  f is open by A1, A2, Th1; ::_thesis: verum
end;

theorem :: TOPS_4:8
for m being Nat
for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
proof
let m be Nat; ::_thesis: for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let T be non empty TopSpace; ::_thesis: for f being Function of (TOP-REAL m),T holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
let f be Function of (TOP-REAL m),T; ::_thesis: ( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),T ;
A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;
A3: m in NAT by ORDINAL1:def_12;
thus  ( f is open implies for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ) ::_thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open )
proof
assume A4: f is open ; ::_thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
reconsider q = p as Point of (Euclid m) by EUCLID:67;
 f1 is open by A4, A1, A2, Th1;
then consider W being open Subset of T such that
A5: ( f1 . p in W & W c= f1 .: (Ball (q,r)) ) by Th5;
 Ball (p,r) = Ball (q,r) by A3, TOPREAL9:13;
hence  ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) by A5; ::_thesis: verum
end;
assume A6: for p being Point of (TOP-REAL m)
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) ; ::_thesis: f is open
 for p being Point of (Euclid m)
for r being real positive number ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball (p,r)) )
proof
let p be Point of (Euclid m); ::_thesis: for r being real positive number ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball (p,r)) )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball (p,r)) )
reconsider q = p as Point of (TOP-REAL m) by EUCLID:67;
consider W being open Subset of T such that
A7: ( f . q in W & W c= f .: (Ball (q,r)) ) by A6;
 Ball (p,r) = Ball (q,r) by A3, TOPREAL9:13;
hence  ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball (p,r)) ) by A7; ::_thesis: verum
end;
then  f1 is open by Th5;
hence  f is open by A1, A2, Th1; ::_thesis: verum
end;

theorem :: TOPS_4:9
for m, n being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) )
proof
let m, n be Nat; ::_thesis: for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) )
let f be Function of (TOP-REAL m),(TOP-REAL n); ::_thesis: ( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) )
A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def_8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ;
A2: ( m in NAT & n in NAT ) by ORDINAL1:def_12;
thus  ( f is open implies for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) ::_thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) implies f is open )
proof
assume A3: f is open ; ::_thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r))
let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r))
let r be real positive number ; ::_thesis: ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r))
reconsider p1 = p as Point of (Euclid m) by EUCLID:67;
reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67;
 f1 is open by A1, A3, Th1;
then consider s being real positive number  such that
A4: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6;
 ( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball ((f . p),s) ) by A2, TOPREAL9:13;
hence  ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) by A4; ::_thesis: verum
end;
assume A5: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ; ::_thesis: f is open
 for p being Point of (Euclid m)
for q being Point of (Euclid n)
for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
proof
let p be Point of (Euclid m); ::_thesis: for q being Point of (Euclid n)
for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
let q be Point of (Euclid n); ::_thesis: for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) )
assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;
reconsider q1 = q as Point of (TOP-REAL n) by EUCLID:67;
consider s being real positive number  such that
A7: Ball (q1,s) c= f .: (Ball (p1,r)) by A5, A6;
 ( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball (q,s) ) by A2, TOPREAL9:13;
hence  ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) by A7; ::_thesis: verum
end;
then  f1 is open by Th6;
hence  f is open by A1, Th1; ::_thesis: verum
end;

theorem :: TOPS_4:10
for T being non empty TopSpace
for f being Function of T,R^1 holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 holds
( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V )
let f be Function of T,R^1; ::_thesis: ( f is open iff for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V )
thus  ( f is open implies for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) ::_thesis: ( ( for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V
let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V
let V be open Subset of T; ::_thesis: ( p in V implies ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V )
assume A2: p in V ; ::_thesis: ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V
reconsider fp = f . p as Point of RealSpace ;
consider r being real positive number  such that
A3: Ball (fp,r) c= f .: V by A1, A2, Th4;
 r in REAL by XREAL_0:def_1;
then  ].(fp - r),(fp + r).[ = Ball (fp,r) by FRECHET:7;
hence  ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V by A3; ::_thesis: verum
end;
assume A4: for p being Point of T
for V being open Subset of T st p in V holds
ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ; ::_thesis: f is open
 for p being Point of T
for V being open Subset of T
for q being Point of RealSpace st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
proof
let p be Point of T; ::_thesis: for V being open Subset of T
for q being Point of RealSpace st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let V be open Subset of T; ::_thesis: for q being Point of RealSpace st q = f . p & p in V holds
ex r being real positive number st Ball (q,r) c= f .: V
let q be Point of RealSpace; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V )
assume A5: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V )
assume  p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V
then consider r being real positive number  such that
A6: ].((f . p) - r),((f . p) + r).[ c= f .: V by A4;
 r in REAL by XREAL_0:def_1;
then  ].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;
hence  ex r being real positive number st Ball (q,r) c= f .: V by A5, A6; ::_thesis: verum
end;
hence  f is open by Th4; ::_thesis: verum
end;

theorem :: TOPS_4:11
for T being non empty TopSpace
for f being Function of R^1,T holds
( f is open iff for p being Point of R^1
for r being real positive number ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of R^1,T holds
( f is open iff for p being Point of R^1
for r being real positive number ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )
let f be Function of R^1,T; ::_thesis: ( f is open iff for p being Point of R^1
for r being real positive number ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) )
thus  ( f is open implies for p being Point of R^1
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ) ::_thesis: ( ( for p being Point of R^1
for r being real positive number ex V being open Subset of T st
( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of R^1
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ )
let p be Point of R^1; ::_thesis: for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ )
reconsider q = p as Point of RealSpace ;
consider W being open Subset of T such that
A2: ( f . p in W & W c= f .: (Ball (q,r)) ) by A1, Th5;
 r in REAL by XREAL_0:def_1;
then  ].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7;
hence  ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ ) by A2; ::_thesis: verum
end;
assume A3: for p being Point of R^1
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ; ::_thesis: f is open
 for p being Point of RealSpace
for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
proof
let p be Point of RealSpace; ::_thesis: for r being real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) )
reconsider q = p as Point of R^1 ;
consider W being open Subset of T such that
A4: ( f . q in W & W c= f .: ].(p - r),(p + r).[ ) by A3;
 r in REAL by XREAL_0:def_1;
then  ].(p - r),(p + r).[ = Ball (p,r) by FRECHET:7;
hence  ex W being open Subset of T st
( f . p in W & W c= f .: (Ball (p,r)) ) by A4; ::_thesis: verum
end;
hence  f is open by Th5; ::_thesis: verum
end;

theorem :: TOPS_4:12
for f being Function of R^1,R^1 holds
( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ )
proof
let f be Function of R^1,R^1; ::_thesis: ( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ )
thus  ( f is open implies for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) ::_thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) implies f is open )
proof
assume A1: f is open ; ::_thesis: for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
let r be real positive number ; ::_thesis: ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
reconsider p1 = p, q1 = f . p as Point of RealSpace ;
consider s being real positive number  such that
A2: Ball (q1,s) c= f .: (Ball (p1,r)) by A1, Th6;
 ( r in REAL & s in REAL ) by XREAL_0:def_1;
then  ( ].(p - r),(p + r).[ = Ball (p1,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q1,s) ) by FRECHET:7;
hence  ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A2; ::_thesis: verum
end;
assume A3: for p being Point of R^1
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ; ::_thesis: f is open
 for p, q being Point of RealSpace
for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
proof
let p, q be Point of RealSpace; ::_thesis: for r being real positive number st q = f . p holds
ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) )
assume A4: q = f . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r))
consider s being real positive number  such that
A5: ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A3;
 ( r in REAL & s in REAL ) by XREAL_0:def_1;
then  ( ].(p - r),(p + r).[ = Ball (p,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q,s) ) by A4, FRECHET:7;
hence  ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) by A5; ::_thesis: verum
end;
hence  f is open by Th6; ::_thesis: verum
end;

theorem :: TOPS_4:13
for m being Nat
for f being Function of (TOP-REAL m),R^1 holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
proof
let m be Nat; ::_thesis: for f being Function of (TOP-REAL m),R^1 holds
( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
let f be Function of (TOP-REAL m),R^1; ::_thesis: ( f is open iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) )
A1: m in NAT by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) implies f is open )
assume A2: f is open ; ::_thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
let r be real positive number ; ::_thesis: ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
 p in Ball (p,r) by A1, TOPGEN_5:13;
then A3: f . p in f .: (Ball (p,r)) by FUNCT_2:35;
 f .: (Ball (p,r)) is open by A2, T_0TOPSP:def_2;
then consider s being Element of REAL  such that
A4: s > 0 and
A5: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A3, FRECHET:8;
reconsider s = s as real positive number by A4;
take s = s; ::_thesis: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r))
thus  ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A5; ::_thesis: verum
end;
assume A6: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ; ::_thesis: f is open
let A be Subset of (TOP-REAL m); :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
assume A7: A is open ; ::_thesis: f .: A is open
 for x being set holds
( x in f .: A iff ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) )
proof
let x be set ; ::_thesis: ( x in f .: A iff ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) )
hereby  ::_thesis: ( ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )
assume  x in f .: A ; ::_thesis: ex Q being Element of K6( the U1 of K414()) st
( Q is open & Q c= f .: A & x in Q )
then consider p being Point of (TOP-REAL m) such that
A8: p in A and
A9: x = f . p by FUNCT_2:65;
reconsider u = p as Point of (Euclid m) by EUCLID:67;
 A = Int A by A7, TOPS_1:23;
then consider e being real number  such that
A10: e > 0 and
A11: Ball (u,e) c= A by A8, GOBOARD6:5;
A12: Ball (u,e) = Ball (p,e) by A1, TOPREAL9:13;
consider s being real positive number  such that
A13: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,e)) by A6, A10;
take Q = R^1 ].((f . p) - s),((f . p) + s).[; ::_thesis: ( Q is open & Q c= f .: A & x in Q )
thus  Q is open ; ::_thesis: ( Q c= f .: A & x in Q )
 f .: (Ball (p,e)) c= f .: A by A11, A12, RELAT_1:123;
hence  Q c= f .: A by A13, XBOOLE_1:1; ::_thesis: x in Q
thus  x in Q by A9, TOPREAL6:15; ::_thesis: verum
end;
thus  ( ex Q being Subset of R^1 st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; ::_thesis: verum
end;
hence  f .: A is open by TOPS_1:25; ::_thesis: verum
end;

theorem :: TOPS_4:14
for m being Nat
for f being Function of R^1,(TOP-REAL m) holds
( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
proof
let m be Nat; ::_thesis: for f being Function of R^1,(TOP-REAL m) holds
( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
let f be Function of R^1,(TOP-REAL m); ::_thesis: ( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider f1 = f as Function of R^1,(TopSpaceMetr (Euclid m)) ;
A2: m in NAT by ORDINAL1:def_12;
thus  ( f is open implies for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) ::_thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) implies f is open )
proof
assume A3: f is open ; ::_thesis: for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
let r be real positive number ; ::_thesis: ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
reconsider p1 = p as Point of RealSpace ;
reconsider q1 = f . p as Point of (Euclid m) by EUCLID:67;
 f1 is open by A1, A3, Th1;
then consider s being real positive number  such that
A4: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6;
 r in REAL by XREAL_0:def_1;
then  ( ].(p - r),(p + r).[ = Ball (p1,r) & Ball ((f . p),s) = Ball (q1,s) ) by A2, FRECHET:7, TOPREAL9:13;
hence  ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ by A4; ::_thesis: verum
end;
assume A5: for p being Point of R^1
for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ; ::_thesis: f is open
 for p being Point of RealSpace
for q being Point of (Euclid m)
for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
proof
let p be Point of RealSpace; ::_thesis: for q being Point of (Euclid m)
for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
let q be Point of (Euclid m); ::_thesis: for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) )
assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r))
reconsider p1 = p as Point of R^1 ;
consider s being real positive number  such that
A7: Ball ((f . p1),s) c= f .: ].(p1 - r),(p1 + r).[ by A5;
 ( r in REAL & s in REAL ) by XREAL_0:def_1;
then  ( ].(p1 - r),(p1 + r).[ = Ball (p,r) & Ball ((f . p1),s) = Ball (q,s) ) by A2, A6, FRECHET:7, TOPREAL9:13;
hence  ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) by A7; ::_thesis: verum
end;
then  f1 is open by Th6;
hence  f is open by A1, Th1; ::_thesis: verum
end;

begin

theorem :: TOPS_4:15
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is continuous iff for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
proof
let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is continuous iff for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
let M be non empty MetrSpace; ::_thesis: for f being Function of T,(TopSpaceMetr M) holds
( f is continuous iff for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
let f be Function of T,(TopSpaceMetr M); ::_thesis: ( f is continuous iff for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
thus  ( f is continuous implies for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) ) ::_thesis: ( ( for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) ) implies f is continuous )
proof
assume A1: f is continuous ; ::_thesis: for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) )
let p be Point of T; ::_thesis: for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) )
let q be Point of M; ::_thesis: for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) )
let r be real positive number ; ::_thesis: ( q = f . p implies ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) )
assume A2: f . p = q ; ::_thesis: ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) )
reconsider V = Ball (q,r) as Subset of (TopSpaceMetr M) ;
A3: q in Ball (q,r) by GOBOARD6:1;
 V is open by TOPMETR:14;
then  ex W being Subset of T st
( p in W & W is open & f .: W c= V ) by A1, A2, A3, JGRAPH_2:10;
hence  ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) ; ::_thesis: verum
end;
assume A4: for p being Point of T
for q being Point of M
for r being real positive number st q = f . p holds
ex W being open Subset of T st
( p in W & f .: W c= Ball (q,r) ) ; ::_thesis: f is continuous
 for p being Point of T
for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
proof
let p be Point of T; ::_thesis: for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
let V be Subset of (TopSpaceMetr M); ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
assume A5: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
reconsider u = f . p as Point of M ;
assume  V is open ; ::_thesis: ex W being Subset of T st
( p in W & W is open & f .: W c= V )
then  Int V = V by TOPS_1:23;
then consider e being real number  such that
A6: ( e > 0 & Ball (u,e) c= V ) by A5, GOBOARD6:4;
 ex W being open Subset of T st
( p in W & f .: W c= Ball (u,e) ) by A4, A6;
hence  ex W being Subset of T st
( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem :: TOPS_4:16
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
proof
let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
let M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M),T holds
( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
let f be Function of (TopSpaceMetr M),T; ::_thesis: ( f is continuous iff for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
hereby  ::_thesis: ( ( for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V
let p be Point of M; ::_thesis: for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V
let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: (Ball (p,s)) c= V )
assume  f . p in V ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= V
then consider W being Subset of (TopSpaceMetr M) such that
A2: p in W and
A3: W is open and
A4: f .: W c= V by A1, JGRAPH_2:10;
 Int W = W by A3, TOPS_1:23;
then consider s being real number  such that
A5: s > 0 and
A6: Ball (p,s) c= W by A2, GOBOARD6:4;
reconsider s = s as real positive number by A5;
take s = s; ::_thesis: f .: (Ball (p,s)) c= V
 f .: (Ball (p,s)) c= f .: W by A6, RELAT_1:123;
hence  f .: (Ball (p,s)) c= V by A4, XBOOLE_1:1; ::_thesis: verum
end;
assume A7: for p being Point of M
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V ; ::_thesis: f is continuous
 for p being Point of (TopSpaceMetr M)
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
proof
let p be Point of (TopSpaceMetr M); ::_thesis: for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V ) )
assume that
A8: f . p in V and
A9: V is open ; ::_thesis: ex W being Subset of (TopSpaceMetr M) st
( p in W & W is open & f .: W c= V )
reconsider u = p as Point of M ;
consider s being real positive number  such that
A10: f .: (Ball (u,s)) c= V by A7, A8, A9;
reconsider W = Ball (u,s) as Subset of (TopSpaceMetr M) ;
take  W ; ::_thesis: ( p in W & W is open & f .: W c= V )
thus  p in W by GOBOARD6:1; ::_thesis: ( W is open & f .: W c= V )
thus  W is open by TOPMETR:14; ::_thesis: f .: W c= V
thus  f .: W c= V by A10; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem Th17: :: TOPS_4:17
for M1, M2 being non empty MetrSpace
for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
proof
let M1, M2 be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); ::_thesis: ( f is continuous iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
hereby  ::_thesis: ( ( for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let p be Point of M1; ::_thesis: for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let q be Point of M2; ::_thesis: for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
assume A2: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
 r in REAL by XREAL_0:def_1;
then consider s being Element of REAL  such that
A3: s > 0 and
A4: for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (p,w) < s holds
dist (q,w1) < r by A1, A2, UNIFORM1:4;
reconsider s = s as real positive number by A3;
take s = s; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r)
thus  f .: (Ball (p,s)) c= Ball (q,r) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (Ball (p,s)) or y in Ball (q,r) )
assume  y in f .: (Ball (p,s)) ; ::_thesis: y in Ball (q,r)
then consider x being Point of (TopSpaceMetr M1) such that
A5: x in Ball (p,s) and
A6: f . x = y by FUNCT_2:65;
reconsider x1 = x as Point of M1 ;
reconsider y1 = y as Point of M2 by A6;
 dist (p,x1) < s by A5, METRIC_1:11;
then  dist (q,y1) < r by A6, A4;
hence  y in Ball (q,r) by METRIC_1:11; ::_thesis: verum
end;
end;
assume A7: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ; ::_thesis: f is continuous
 for r being real number
for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
proof
let r be real number ; ::_thesis: for u being Element of M1
for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u be Element of M1; ::_thesis: for u1 being Element of M2 st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u1 be Element of M2; ::_thesis: ( r > 0 & u1 = f . u implies ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
assume  ( r > 0 & u1 = f . u ) ; ::_thesis: ex s being real number st
( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
then consider s being real positive number  such that
A8: f .: (Ball (u,s)) c= Ball (u1,r) by A7;
take  s ; ::_thesis: ( s > 0 & ( for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
thus  s > 0 ; ::_thesis: for w being Element of M1
for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r
let w be Element of M1; ::_thesis: for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds
dist (u1,w1) < r
let w1 be Element of M2; ::_thesis: ( w1 = f . w & dist (u,w) < s implies dist (u1,w1) < r )
assume A9: w1 = f . w ; ::_thesis: ( not dist (u,w) < s or dist (u1,w1) < r )
assume  dist (u,w) < s ; ::_thesis: dist (u1,w1) < r
then  w in Ball (u,s) by METRIC_1:11;
then  f . w in f .: (Ball (u,s)) by FUNCT_2:35;
hence  dist (u1,w1) < r by A8, A9, METRIC_1:11; ::_thesis: verum
end;
hence  f is continuous by UNIFORM1:3; ::_thesis: verum
end;

theorem :: TOPS_4:18
for m being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
proof
let m be Nat; ::_thesis: for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
let f be Function of T,(TOP-REAL m); ::_thesis: ( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )
A1: m in NAT by ORDINAL1:def_12;
thus  ( f is continuous implies for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ) ::_thesis: ( ( for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ) implies f is continuous )
proof
assume A2: f is continuous ; ::_thesis: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
let p be Point of T; ::_thesis: for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) )
 f . p in Ball ((f . p),r) by A1, TOPGEN_5:13;
then  ex W being Subset of T st
( p in W & W is open & f .: W c= Ball ((f . p),r) ) by A2, JGRAPH_2:10;
hence  ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ; ::_thesis: verum
end;
assume A3: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) ; ::_thesis: f is continuous
 for p being Point of T
for V being Subset of (TOP-REAL m) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
proof
let p be Point of T; ::_thesis: for V being Subset of (TOP-REAL m) st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
let V be Subset of (TOP-REAL m); ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
assume A4: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
reconsider u = f . p as Point of (Euclid m) by EUCLID:67;
assume  V is open ; ::_thesis: ex W being Subset of T st
( p in W & W is open & f .: W c= V )
then  Int V = V by TOPS_1:23;
then consider e being real number  such that
A5: e > 0 and
A6: Ball (u,e) c= V by A4, GOBOARD6:5;
A7: Ball (u,e) = Ball ((f . p),e) by A1, TOPREAL9:13;
 ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),e) ) by A3, A5;
hence  ex W being Subset of T st
( p in W & W is open & f .: W c= V ) by A6, A7, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem :: TOPS_4:19
for m being Nat
for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
proof
let m be Nat; ::_thesis: for T being non empty TopSpace
for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
let T be non empty TopSpace; ::_thesis: for f being Function of (TOP-REAL m),T holds
( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
let f be Function of (TOP-REAL m),T; ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V )
A1: m in NAT by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V
let p be Point of (TOP-REAL m); ::_thesis: for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V
let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: (Ball (p,s)) c= V )
assume  f . p in V ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= V
then consider W being Subset of (TOP-REAL m) such that
A3: p in W and
A4: W is open and
A5: f .: W c= V by A2, JGRAPH_2:10;
reconsider u = p as Point of (Euclid m) by EUCLID:67;
 Int W = W by A4, TOPS_1:23;
then consider s being real number  such that
A6: s > 0 and
A7: Ball (u,s) c= W by A3, GOBOARD6:5;
reconsider s = s as real positive number by A6;
take s = s; ::_thesis: f .: (Ball (p,s)) c= V
 Ball (u,s) = Ball (p,s) by A1, TOPREAL9:13;
then  f .: (Ball (p,s)) c= f .: W by A7, RELAT_1:123;
hence  f .: (Ball (p,s)) c= V by A5, XBOOLE_1:1; ::_thesis: verum
end;
assume A8: for p being Point of (TOP-REAL m)
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: (Ball (p,s)) c= V ; ::_thesis: f is continuous
 for p being Point of (TOP-REAL m)
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V )
proof
let p be Point of (TOP-REAL m); ::_thesis: for V being Subset of T st f . p in V & V is open holds
ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V )
let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V ) )
assume that
A9: f . p in V and
A10: V is open ; ::_thesis: ex W being Subset of (TOP-REAL m) st
( p in W & W is open & f .: W c= V )
consider s being real positive number  such that
A11: f .: (Ball (p,s)) c= V by A8, A9, A10;
take W = Ball (p,s); ::_thesis: ( p in W & W is open & f .: W c= V )
thus  p in W by A1, TOPGEN_5:13; ::_thesis: ( W is open & f .: W c= V )
thus  W is open ; ::_thesis: f .: W c= V
thus  f .: W c= V by A11; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem :: TOPS_4:20
for m, n being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) )
proof
let m, n be Nat; ::_thesis: for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) )
let f be Function of (TOP-REAL m),(TOP-REAL n); ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) )
A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def_8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ;
A2: ( m in NAT & n in NAT ) by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ) implies f is continuous )
assume A3: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r)
let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r)
let r be real positive number ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r)
reconsider p1 = p as Point of (Euclid m) by EUCLID:67;
reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67;
 f1 is continuous by A1, A3, YELLOW12:36;
then consider s being real positive number  such that
A4: f1 .: (Ball (p1,s)) c= Ball (q1,r) by Th17;
take s = s; ::_thesis: f .: (Ball (p,s)) c= Ball ((f . p),r)
 ( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = Ball ((f . p),r) ) by A2, TOPREAL9:13;
hence  f .: (Ball (p,s)) c= Ball ((f . p),r) by A4; ::_thesis: verum
end;
assume A5: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ; ::_thesis: f is continuous
 for p being Point of (Euclid m)
for q being Point of (Euclid n)
for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
proof
let p be Point of (Euclid m); ::_thesis: for q being Point of (Euclid n)
for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
let q be Point of (Euclid n); ::_thesis: for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) )
assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;
consider s being real positive number  such that
A7: f .: (Ball (p1,s)) c= Ball ((f . p1),r) by A5;
take  s ; ::_thesis: f1 .: (Ball (p,s)) c= Ball (q,r)
 ( Ball (p1,s) = Ball (p,s) & Ball ((f . p1),r) = Ball (q,r) ) by A2, A6, TOPREAL9:13;
hence  f1 .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum
end;
then  f1 is continuous by Th17;
hence  f is continuous by A1, YELLOW12:36; ::_thesis: verum
end;

theorem :: TOPS_4:21
for T being non empty TopSpace
for f being Function of T,R^1 holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 holds
( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )
let f be Function of T,R^1; ::_thesis: ( f is continuous iff for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) )
thus  ( f is continuous implies for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) ::_thesis: ( ( for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) implies f is continuous )
proof
assume A1: f is continuous ; ::_thesis: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )
let p be Point of T; ::_thesis: for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )
let r be real positive number ; ::_thesis: ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ )
A2: f . p in ].((f . p) - r),((f . p) + r).[ by TOPREAL6:15;
 R^1 ].((f . p) - r),((f . p) + r).[ is open ;
then  ex W being Subset of T st
( p in W & W is open & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A1, A2, JGRAPH_2:10;
hence  ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; ::_thesis: verum
end;
assume A3: for p being Point of T
for r being real positive number ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; ::_thesis: f is continuous
 for p being Point of T
for V being Subset of R^1 st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
proof
let p be Point of T; ::_thesis: for V being Subset of R^1 st f . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & f .: W c= V )
let V be Subset of R^1; ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
assume A4: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st
( p in W & W is open & f .: W c= V ) )
assume  V is open ; ::_thesis: ex W being Subset of T st
( p in W & W is open & f .: W c= V )
then consider r being Element of REAL  such that
A5: r > 0 and
A6: ].((f . p) - r),((f . p) + r).[ c= V by A4, FRECHET:8;
 ex W being open Subset of T st
( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A3, A5;
hence  ex W being Subset of T st
( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem :: TOPS_4:22
for T being non empty TopSpace
for f being Function of R^1,T holds
( f is continuous iff for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V )
proof
let T be non empty TopSpace; ::_thesis: for f being Function of R^1,T holds
( f is continuous iff for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V )
let f be Function of R^1,T; ::_thesis: ( f is continuous iff for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V )
hereby  ::_thesis: ( ( for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V
let p be Point of R^1; ::_thesis: for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V
let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: ].(p - s),(p + s).[ c= V )
assume  f . p in V ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= V
then consider W being Subset of R^1 such that
A2: p in W and
A3: W is open and
A4: f .: W c= V by A1, JGRAPH_2:10;
consider s being Element of REAL  such that
A5: s > 0 and
A6: ].(p - s),(p + s).[ c= W by A2, A3, FRECHET:8;
reconsider s = s as real positive number by A5;
take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= V
 f .: ].(p - s),(p + s).[ c= f .: W by A6, RELAT_1:123;
hence  f .: ].(p - s),(p + s).[ c= V by A4, XBOOLE_1:1; ::_thesis: verum
end;
assume A7: for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ; ::_thesis: f is continuous
 for p being Point of R^1
for V being Subset of T st f . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & f .: W c= V )
proof
let p be Point of R^1; ::_thesis: for V being Subset of T st f . p in V & V is open holds
ex W being Subset of R^1 st
( p in W & W is open & f .: W c= V )
let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of R^1 st
( p in W & W is open & f .: W c= V ) )
assume that
A8: f . p in V and
A9: V is open ; ::_thesis: ex W being Subset of R^1 st
( p in W & W is open & f .: W c= V )
consider s being real positive number  such that
A10: f .: ].(p - s),(p + s).[ c= V by A7, A8, A9;
take W = R^1 ].(p - s),(p + s).[; ::_thesis: ( p in W & W is open & f .: W c= V )
thus  p in W by TOPREAL6:15; ::_thesis: ( W is open & f .: W c= V )
thus  W is open ; ::_thesis: f .: W c= V
thus  f .: W c= V by A10; ::_thesis: verum
end;
hence  f is continuous by JGRAPH_2:10; ::_thesis: verum
end;

theorem :: TOPS_4:23
for f being Function of R^1,R^1 holds
( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ )
proof
let f be Function of R^1,R^1; ::_thesis: ( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ )
hereby  ::_thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
let r be real positive number ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
reconsider p1 = p, q1 = f . p as Point of RealSpace ;
consider s being real positive number  such that
A2: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17;
take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
 ( p1 in REAL & q1 in REAL & r in REAL & s in REAL ) by XREAL_0:def_1;
then  ( Ball (p1,s) = ].(p1 - s),(p1 + s).[ & Ball (q1,r) = ].(q1 - r),(q1 + r).[ ) by FRECHET:7;
hence  f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ by A2; ::_thesis: verum
end;
assume A3: for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ; ::_thesis: f is continuous
 for p, q being Point of RealSpace
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
proof
let p, q be Point of RealSpace; ::_thesis: for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
assume A4: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
consider s being real positive number  such that
A5: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ by A3;
take  s ; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r)
 ( p in REAL & q in REAL & r in REAL & s in REAL ) by XREAL_0:def_1;
then  ( Ball (p,s) = ].(p - s),(p + s).[ & Ball (q,r) = ].(q - r),(q + r).[ ) by FRECHET:7;
hence  f .: (Ball (p,s)) c= Ball (q,r) by A5, A4; ::_thesis: verum
end;
hence  f is continuous by Th17; ::_thesis: verum
end;

theorem :: TOPS_4:24
for m being Nat
for f being Function of (TOP-REAL m),R^1 holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )
proof
let m be Nat; ::_thesis: for f being Function of (TOP-REAL m),R^1 holds
( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )
let f be Function of (TOP-REAL m),R^1; ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),R^1 ;
A2: m in NAT by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )
assume A3: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[
let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[
let r be real positive number ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[
reconsider p1 = p as Point of (Euclid m) by EUCLID:67;
reconsider q1 = f . p as Point of RealSpace ;
 f1 is continuous by A1, A3, YELLOW12:36;
then consider s being real positive number  such that
A4: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17;
take s = s; ::_thesis: f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[
 ( q1 in REAL & r in REAL ) by XREAL_0:def_1;
then  ( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = ].((f . p) - r),((f . p) + r).[ ) by A2, FRECHET:7, TOPREAL9:13;
hence  f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ by A4; ::_thesis: verum
end;
assume A5: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ; ::_thesis: f is continuous
 for p being Point of (Euclid m)
for q being Point of RealSpace
for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
proof
let p be Point of (Euclid m); ::_thesis: for q being Point of RealSpace
for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
let q be Point of RealSpace; ::_thesis: for r being real positive number st q = f1 . p holds
ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) )
assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r)
reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;
consider s being real positive number  such that
A7: f .: (Ball (p1,s)) c= ].((f . p) - r),((f . p) + r).[ by A5;
take  s ; ::_thesis: f1 .: (Ball (p,s)) c= Ball (q,r)
 ( q in REAL & r in REAL ) by XREAL_0:def_1;
then  ( Ball (p1,s) = Ball (p,s) & ].((f . p) - r),((f . p) + r).[ = Ball (q,r) ) by A2, A6, FRECHET:7, TOPREAL9:13;
hence  f1 .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum
end;
then  f1 is continuous by Th17;
hence  f is continuous by A1, YELLOW12:36; ::_thesis: verum
end;

theorem :: TOPS_4:25
for m being Nat
for f being Function of R^1,(TOP-REAL m) holds
( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )
proof
let m be Nat; ::_thesis: for f being Function of R^1,(TOP-REAL m) holds
( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )
let f be Function of R^1,(TOP-REAL m); ::_thesis: ( f is continuous iff for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )
A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8;
then reconsider f1 = f as Function of R^1,(TopSpaceMetr (Euclid m)) ;
A2: m in NAT by ORDINAL1:def_12;
hereby  ::_thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ) implies f is continuous )
assume A3: f is continuous ; ::_thesis: for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r)
let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r)
let r be real positive number ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r)
reconsider p1 = p as Point of RealSpace ;
reconsider q1 = f . p as Point of (Euclid m) by EUCLID:67;
 f1 is continuous by A1, A3, YELLOW12:36;
then consider s being real positive number  such that
A4: f1 .: (Ball (p1,s)) c= Ball (q1,r) by Th17;
take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= Ball ((f . p),r)
 ( p in REAL & s in REAL ) by XREAL_0:def_1;
then  ( Ball (p1,s) = ].(p - s),(p + s).[ & Ball (q1,r) = Ball ((f . p),r) ) by A2, FRECHET:7, TOPREAL9:13;
hence  f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) by A4; ::_thesis: verum
end;
assume A5: for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ; ::_thesis: f is continuous
 for p being Point of RealSpace
for q being Point of (Euclid m)
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
proof
let p be Point of RealSpace; ::_thesis: for q being Point of (Euclid m)
for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let q be Point of (Euclid m); ::_thesis: for r being real positive number st q = f . p holds
ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) )
assume A6: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r)
reconsider p1 = p as Point of R^1 ;
consider s being real positive number  such that
A7: f .: ].(p - s),(p + s).[ c= Ball ((f . p1),r) by A5;
take  s ; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r)
 ( p in REAL & s in REAL ) by XREAL_0:def_1;
then  ( ].(p - s),(p + s).[ = Ball (p,s) & Ball ((f . p1),r) = Ball (q,r) ) by A2, A6, FRECHET:7, TOPREAL9:13;
hence  f .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum
end;
then  f1 is continuous by A1, Th17;
hence  f is continuous by A1, YELLOW12:36; ::_thesis: verum
end;