:: On the Continuity of Some Functions
:: by Artur Korni{\l}owicz
::
:: Received February 9, 2010
:: Copyright (c) 2010 Association of Mizar Users


begin

registration
let R be Relation;
let X be empty set ;
cluster R .: X -> empty ;
coherence
R .: X is empty by RELAT_1:149;
cluster R " X -> empty ;
coherence
R " X is empty by RELAT_1:171;
end;

registration
let A be empty set ;
cluster -> empty Element of A;
coherence
for b1 being Element of A holds b1 is empty by SUBSET_1:def 2;
end;

theorem :: TOPREALC:1
for X being trivial set
for Y being set st X,Y are_equipotent holds
Y is trivial
proof end;

registration
let r be real number ;
cluster r ^2 -> non negative ;
coherence
not r ^2 is negative ;
end;

registration
let r be real positive number ;
cluster r ^2 -> positive ;
coherence
r ^2 is positive ;
end;

registration
cluster sqrt 0 -> zero ;
coherence
sqrt 0 is empty by SQUARE_1:82;
end;

registration
let f be empty set ;
cluster f ^2 -> empty ;
coherence
sqr f is empty ;
cluster |.f.| -> zero ;
coherence
|.f.| is empty by RVSUM_1:102;
end;

theorem Th2: :: TOPREALC:2
for c1, c2 being complex number
for f being complex-valued Function holds f (#) (c1 + c2) = (f (#) c1) + (f (#) c2)
proof end;

theorem :: TOPREALC:3
for c1, c2 being complex number
for f being complex-valued Function holds f (#) (c1 - c2) = (f (#) c1) - (f (#) c2)
proof end;

theorem Th4: :: TOPREALC:4
for c being complex number
for f, g being complex-valued Function holds (f (/) c) + (g (/) c) = (f + g) (/) c
proof end;

theorem :: TOPREALC:5
for c being complex number
for f, g being complex-valued Function holds (f (/) c) - (g (/) c) = (f - g) (/) c
proof end;

theorem :: TOPREALC:6
for c1, c2 being complex number
for f, g being complex-valued Function st c1 <> 0 & c2 <> 0 holds
(f (/) c1) - (g (/) c2) = ((f (#) c2) - (g (#) c1)) (/) (c1 * c2)
proof end;

theorem :: TOPREALC:7
for c being complex number
for f, g being complex-valued Function st c <> 0 holds
(f (/) c) - g = (f - (c (#) g)) (/) c
proof end;

theorem :: TOPREALC:8
for c, d being complex number
for f being complex-valued Function holds (c - d) (#) f = (c (#) f) - (d (#) f)
proof end;

theorem :: TOPREALC:9
for f, g being complex-valued Function holds (f - g) ^2 = (g - f) ^2
proof end;

theorem :: TOPREALC:10
for c being complex number
for f being complex-valued Function holds (f (/) c) ^2 = (f ^2 ) (/) (c ^2 )
proof end;

theorem Th11: :: TOPREALC:11
for n being Nat
for r, s being real number holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * (abs (r - s))
proof end;

registration
let f be complex-valued Function;
let x be set ;
let c be complex number ;
cluster f +* x,c -> complex-valued ;
coherence
f +* x,c is complex-valued
proof end;
end;

theorem Th12: :: TOPREALC:12
for x being set
for n being Nat
for c being complex number holds ((0* n) +* x,c) ^2 = (0* n) +* x,(c ^2 )
proof end;

theorem Th13: :: TOPREALC:13
for x being set
for n being Nat
for r being real number st x in Seg n holds
|.((0* n) +* x,r).| = abs r
proof end;

theorem Th14: :: TOPREALC:14
for x being set
for n being Nat holds (0.REAL n) +* x,0 = 0.REAL n
proof end;

theorem Th15: :: TOPREALC:15
for x being set
for n being Nat
for r being real number
for f1 being real-valued b2 -long FinSequence holds mlt f1,((0.REAL n) +* x,r) = (0.REAL n) +* x,((f1 . x) * r)
proof end;

theorem :: TOPREALC:16
for x being set
for n being Nat
for r being real number
for f1 being real-valued b2 -long FinSequence holds |(f1,((0.REAL n) +* x,r))| = (f1 . x) * r
proof end;

theorem Th17: :: TOPREALC:17
for i, n being Nat
for c being complex number
for g1 being complex-valued b2 -long FinSequence holds (g1 +* i,c) - g1 = (0* n) +* i,(c - (g1 . i))
proof end;

theorem :: TOPREALC:18
for r being real number holds |.<*r*>.| = abs r
proof end;

theorem Th19: :: TOPREALC:19
for f being real-valued FinSequence holds f is FinSequence of REAL
proof end;

theorem :: TOPREALC:20
for f being real-valued FinSequence st |.f.| <> 0 holds
ex i being Nat st
( i in dom f & f . i <> 0 )
proof end;

theorem Th21: :: TOPREALC:21
for f being real-valued FinSequence holds abs (Sum f) <= Sum (abs f)
proof end;

Lm2: for n being Nat
for f being real-valued b1 -long FinSequence holds f is Element of n -tuples_on REAL
proof end;

theorem :: TOPREALC:22
for A being non empty 1-sorted
for B being non empty trivial 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t
proof end;

registration
let n be non zero Nat;
let i be Element of Seg n;
let T be non empty real-membered TopSpace;
cluster proj ((Seg n) --> T),i -> real-valued ;
coherence
proj ((Seg n) --> T),i is real-valued
proof end;
end;

definition
let n be Nat;
let p be Element of REAL n;
let r be real number ;
:: original: (/)
redefine func p (/) r -> Element of REAL n;
coherence
p (/) r is Element of REAL n
proof end;
end;

theorem Th23: :: TOPREALC:23
for m being Nat
for r being real number
for p, q being Point of (TOP-REAL m) holds
( p in Ball q,r iff - p in Ball (- q),r )
proof end;

definition
let S be 1-sorted ;
attr S is complex-functions-membered means :Def1: :: TOPREALC:def 1
the carrier of S is complex-functions-membered ;
attr S is real-functions-membered means :Def2: :: TOPREALC:def 2
the carrier of S is real-functions-membered ;
end;

:: deftheorem Def1 defines complex-functions-membered TOPREALC:def 1 :
for S being 1-sorted holds
( S is complex-functions-membered iff the carrier of S is complex-functions-membered );

:: deftheorem Def2 defines real-functions-membered TOPREALC:def 2 :
for S being 1-sorted holds
( S is real-functions-membered iff the carrier of S is real-functions-membered );

registration
let n be Nat;
cluster TOP-REAL n -> real-functions-membered ;
coherence
TOP-REAL n is real-functions-membered
proof end;
end;

registration
cluster TOP-REAL 0 -> real-membered ;
coherence
TOP-REAL 0 is real-membered
proof end;
end;

registration
cluster TOP-REAL 0 -> trivial ;
coherence
TOP-REAL 0 is trivial by EUCLID:25, JORDAN2C:113;
end;

registration
cluster real-functions-membered -> complex-functions-membered 1-sorted ;
coherence
for b1 being 1-sorted st b1 is real-functions-membered holds
b1 is complex-functions-membered
proof end;
end;

registration
cluster strict non empty real-functions-membered 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is empty & b1 is real-functions-membered )
proof end;
end;

registration
let S be complex-functions-membered 1-sorted ;
cluster the carrier of S -> complex-functions-membered ;
coherence
the carrier of S is complex-functions-membered by Def1;
end;

registration
let S be real-functions-membered 1-sorted ;
cluster the carrier of S -> real-functions-membered ;
coherence
the carrier of S is real-functions-membered by Def2;
end;

registration
cluster non empty strict real-functions-membered TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & not b1 is empty & b1 is real-functions-membered )
proof end;
end;

registration
let S be complex-functions-membered TopSpace;
cluster -> complex-functions-membered SubSpace of S;
coherence
for b1 being SubSpace of S holds b1 is complex-functions-membered
proof end;
end;

registration
let S be real-functions-membered TopSpace;
cluster -> real-functions-membered SubSpace of S;
coherence
for b1 being SubSpace of S holds b1 is real-functions-membered
proof end;
end;

definition
let X be complex-functions-membered set ;
func (-) X -> complex-functions-membered set means :Def3: :: TOPREALC:def 3
for f being complex-valued Function holds
( - f in it iff f in X );
existence
ex b1 being complex-functions-membered set st
for f being complex-valued Function holds
( - f in b1 iff f in X )
proof end;
uniqueness
for b1, b2 being complex-functions-membered set st ( for f being complex-valued Function holds
( - f in b1 iff f in X ) ) & ( for f being complex-valued Function holds
( - f in b2 iff f in X ) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being complex-functions-membered set st ( for f being complex-valued Function holds
( - f in b1 iff f in b2 ) ) holds
for f being complex-valued Function holds
( - f in b2 iff f in b1 )
proof end;
end;

:: deftheorem Def3 defines (-) TOPREALC:def 3 :
for X, b2 being complex-functions-membered set holds
( b2 = (-) X iff for f being complex-valued Function holds
( - f in b2 iff f in X ) );

registration
let X be empty set ;
cluster (-) X -> empty complex-functions-membered ;
coherence
(-) X is empty
proof end;
end;

registration
let X be non empty complex-functions-membered set ;
cluster (-) X -> non empty complex-functions-membered ;
coherence
not (-) X is empty
proof end;
end;

theorem Th24: :: TOPREALC:24
for X being complex-functions-membered set
for f being complex-valued Function holds
( - f in X iff f in (-) X )
proof end;

registration
let X be real-functions-membered set ;
cluster (-) X -> complex-functions-membered real-functions-membered ;
coherence
(-) X is real-functions-membered
proof end;
end;

theorem Th25: :: TOPREALC:25
for n being Nat
for X being Subset of (TOP-REAL n) holds - X = (-) X
proof end;

definition
let n be Nat;
let X be Subset of (TOP-REAL n);
:: original: (-)
redefine func (-) X -> Subset of (TOP-REAL n);
coherence
(-) X is Subset of (TOP-REAL n)
proof end;
end;

registration
let n be Nat;
let X be open Subset of (TOP-REAL n);
cluster (-) X -> open Subset of (TOP-REAL n);
coherence
for b1 being Subset of (TOP-REAL n) st b1 = (-) X holds
b1 is open
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let x be set ;
:: original: .
redefine func p . x -> Element of REAL ;
coherence
p . x is Element of REAL by XREAL_0:def 1;
end;

definition
let R, S, T be non empty TopSpace;
let f be Function of [:R,S:],T;
let x be Point of [:R,S:];
:: original: .
redefine func f . x -> Point of T;
coherence
f . x is Point of T
proof end;
end;

definition
let R, S, T be non empty TopSpace;
let f be Function of [:R,S:],T;
let r be Point of R;
let s be Point of S;
:: original: .
redefine func f . r,s -> Point of T;
coherence
f . r,s is Point of T
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let r be real number ;
:: original: +
redefine func p + r -> Point of (TOP-REAL n);
coherence
r + p is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let r be real number ;
:: original: -
redefine func p - r -> Point of (TOP-REAL n);
coherence
p - r is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let r be real number ;
:: original: (#)
redefine func p (#) r -> Point of (TOP-REAL n);
coherence
r (#) p is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let r be real number ;
:: original: (/)
redefine func p (/) r -> Point of (TOP-REAL n);
coherence
p (/) r is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original: (#)
redefine func p1 (#) p2 -> Point of (TOP-REAL n);
coherence
p1 (#) p2 is Point of (TOP-REAL n)
proof end;
commutativity
for p1, p2 being Point of (TOP-REAL n) holds p1 (#) p2 = p2 (#) p1 ;
end;

definition
let n be Nat;
let p be Point of (TOP-REAL n);
:: original: ^2
redefine func sqr p -> Point of (TOP-REAL n);
coherence
p ^2 is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original: /"
redefine func p1 /" p2 -> Point of (TOP-REAL n);
coherence
p1 /" p2 is Point of (TOP-REAL n)
proof end;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let x be set ;
let r be real number ;
:: original: +*
redefine func p +* x,r -> Point of (TOP-REAL n);
coherence
p +* x,r is Point of (TOP-REAL n)
proof end;
end;

theorem :: TOPREALC:26
for n being Nat
for r being real number
for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball o,r holds
abs (Sum (a - o)) < n * r
proof end;

registration
let n be Nat;
cluster Euclid n -> real-functions-membered ;
coherence
Euclid n is real-functions-membered
proof end;
end;

theorem :: TOPREALC:27
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V holds (v + u) - u = v
proof end;

theorem :: TOPREALC:28
for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u being Element of V holds (v - u) + u = v
proof end;

theorem Th29: :: TOPREALC:29
for X being set
for c being complex number
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [+] c = f <+> ((dom f) --> c)
proof end;

theorem :: TOPREALC:30
for X being set
for c being complex number
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [-] c = f <-> ((dom f) --> c)
proof end;

theorem Th31: :: TOPREALC:31
for X being set
for c being complex number
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
proof end;

theorem :: TOPREALC:32
for X being set
for c being complex number
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [/] c = f </> ((dom f) --> c)
proof end;

registration
let D be complex-functions-membered set ;
let f, g be FinSequence of D;
cluster f <++> g -> FinSequence-like ;
coherence
f <++> g is FinSequence-like
proof end;
cluster f <--> g -> FinSequence-like ;
coherence
f <--> g is FinSequence-like
proof end;
cluster f <##> g -> FinSequence-like ;
coherence
f <##> g is FinSequence-like
proof end;
cluster f <//> g -> FinSequence-like ;
coherence
f <//> g is FinSequence-like
proof end;
end;

theorem :: TOPREALC:33
for X being set
for n being Nat
for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)
proof end;

theorem Th34: :: TOPREALC:34
for i, n being Nat
for f being Function of (TOP-REAL i),(TOP-REAL n) holds f (-) is Function of (TOP-REAL i),(TOP-REAL n)
proof end;

theorem Th35: :: TOPREALC:35
for X being set
for n being Nat
for r being real number
for f being Function of X,(TOP-REAL n) holds f [+] r is Function of X,(TOP-REAL n)
proof end;

theorem :: TOPREALC:36
for X being set
for n being Nat
for r being real number
for f being Function of X,(TOP-REAL n) holds f [-] r is Function of X,(TOP-REAL n) by Th35;

theorem Th37: :: TOPREALC:37
for X being set
for n being Nat
for r being real number
for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)
proof end;

theorem :: TOPREALC:38
for X being set
for n being Nat
for r being real number
for f being Function of X,(TOP-REAL n) holds f [/] r is Function of X,(TOP-REAL n) by Th37;

theorem Th39: :: TOPREALC:39
for X being set
for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)
proof end;

theorem Th40: :: TOPREALC:40
for X being set
for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <--> g is Function of X,(TOP-REAL n)
proof end;

theorem Th41: :: TOPREALC:41
for X being set
for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <##> g is Function of X,(TOP-REAL n)
proof end;

theorem Th42: :: TOPREALC:42
for X being set
for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <//> g is Function of X,(TOP-REAL n)
proof end;

theorem Th43: :: TOPREALC:43
for X being set
for n being Nat
for f being Function of X,(TOP-REAL n)
for g being Function of X,R^1 holds f <+> g is Function of X,(TOP-REAL n)
proof end;

theorem Th44: :: TOPREALC:44
for X being set
for n being Nat
for f being Function of X,(TOP-REAL n)
for g being Function of X,R^1 holds f <-> g is Function of X,(TOP-REAL n)
proof end;

theorem Th45: :: TOPREALC:45
for X being set
for n being Nat
for f being Function of X,(TOP-REAL n)
for g being Function of X,R^1 holds f <#> g is Function of X,(TOP-REAL n)
proof end;

theorem Th46: :: TOPREALC:46
for X being set
for n being Nat
for f being Function of X,(TOP-REAL n)
for g being Function of X,R^1 holds f </> g is Function of X,(TOP-REAL n)
proof end;

definition
let n be Nat;
let T be non empty set ;
let R be real-membered set ;
let f be Function of T,R;
func incl f,n -> Function of T,(TOP-REAL n) means :Def4: :: TOPREALC:def 4
for t being Element of T holds it . t = n |-> (f . t);
existence
ex b1 being Function of T,(TOP-REAL n) st
for t being Element of T holds b1 . t = n |-> (f . t)
proof end;
uniqueness
for b1, b2 being Function of T,(TOP-REAL n) st ( for t being Element of T holds b1 . t = n |-> (f . t) ) & ( for t being Element of T holds b2 . t = n |-> (f . t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines incl TOPREALC:def 4 :
for n being Nat
for T being non empty set
for R being real-membered set
for f being Function of T,R
for b5 being Function of T,(TOP-REAL n) holds
( b5 = incl f,n iff for t being Element of T holds b5 . t = n |-> (f . t) );

theorem Th47: :: TOPREALC:47
for x being set
for n being Nat
for T being non empty TopSpace
for R being real-membered set
for f being Function of T,R
for t being Point of T st x in Seg n holds
((incl f,n) . t) . x = f . t
proof end;

theorem Th48: :: TOPREALC:48
for T being non empty set
for R being real-membered set
for f being Function of T,R holds incl f,0 = T --> 0
proof end;

theorem Th49: :: TOPREALC:49
for n being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <+> g = f <++> (incl g,n)
proof end;

theorem Th50: :: TOPREALC:50
for n being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <-> g = f <--> (incl g,n)
proof end;

theorem Th51: :: TOPREALC:51
for n being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <#> g = f <##> (incl g,n)
proof end;

theorem :: TOPREALC:52
for n being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f </> g = f <//> (incl g,n)
proof end;

definition
let n be Nat;
set T = TOP-REAL n;
set c = the carrier of (TOP-REAL n);
A1: the carrier of [:(TOP-REAL n),(TOP-REAL n):] = [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] by BORSUK_1:def 5;
func TIMES n -> Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) means :Def5: :: TOPREALC:def 5
for x, y being Point of (TOP-REAL n) holds it . x,y = x (#) y;
existence
ex b1 being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st
for x, y being Point of (TOP-REAL n) holds b1 . x,y = x (#) y
proof end;
uniqueness
for b1, b2 being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st ( for x, y being Point of (TOP-REAL n) holds b1 . x,y = x (#) y ) & ( for x, y being Point of (TOP-REAL n) holds b2 . x,y = x (#) y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines TIMES TOPREALC:def 5 :
for n being Nat
for b2 being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) holds
( b2 = TIMES n iff for x, y being Point of (TOP-REAL n) holds b2 . x,y = x (#) y );

theorem Th53: :: TOPREALC:53
TIMES 0 = [:(TOP-REAL 0 ),(TOP-REAL 0 ):] --> (0. (TOP-REAL 0 ))
proof end;

theorem Th54: :: TOPREALC:54
for n being Nat
for T being non empty TopSpace
for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: f,g
proof end;

definition
let m, n be Nat;
A1: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
func PROJ m,n -> Function of (TOP-REAL m),R^1 means :Def6: :: TOPREALC:def 6
for p being Element of (TOP-REAL m) holds it . p = p /. n;
existence
ex b1 being Function of (TOP-REAL m),R^1 st
for p being Element of (TOP-REAL m) holds b1 . p = p /. n by A1, JORDAN2B:1;
uniqueness
for b1, b2 being Function of (TOP-REAL m),R^1 st ( for p being Element of (TOP-REAL m) holds b1 . p = p /. n ) & ( for p being Element of (TOP-REAL m) holds b2 . p = p /. n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines PROJ TOPREALC:def 6 :
for m, n being Nat
for b3 being Function of (TOP-REAL m),R^1 holds
( b3 = PROJ m,n iff for p being Element of (TOP-REAL m) holds b3 . p = p /. n );

theorem Th55: :: TOPREALC:55
for m, n being Nat
for r being real number
for p being Point of (TOP-REAL m) st n in dom p holds
(PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[
proof end;

theorem :: TOPREALC:56
for T being non empty TopSpace
for m being non zero Nat
for f being Function of T,R^1 holds f = (PROJ m,m) * (incl f,m)
proof end;

begin

registration
let T be non empty TopSpace;
cluster non-empty continuous Element of bool [:the carrier of T,the carrier of R^1 :];
existence
ex b1 being Function of T,R^1 st
( b1 is non-empty & b1 is continuous )
proof end;
end;

theorem :: TOPREALC:57
for n, m being Nat st n in Seg m holds
PROJ m,n is continuous
proof end;

theorem :: TOPREALC:58
for n, m being Nat st n in Seg m holds
PROJ m,n is open
proof end;

registration
let n be Nat;
let T be non empty TopSpace;
let f be continuous Function of T,R^1 ;
cluster incl f,n -> continuous ;
coherence
incl f,n is continuous
proof end;
end;

registration
let n be Nat;
cluster TIMES n -> continuous ;
coherence
TIMES n is continuous
proof end;
end;

theorem :: TOPREALC:59
for m, n being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) st f is continuous holds
f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
proof end;

registration
let T be non empty TopSpace;
let f be continuous Function of T,R^1 ;
cluster - f -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = - f holds
b1 is continuous
proof end;
end;

registration
let T be non empty TopSpace;
let f be non-empty continuous Function of T,R^1 ;
cluster f " -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f " holds
b1 is continuous
proof end;
end;

registration
let T be non empty TopSpace;
let f be continuous Function of T,R^1 ;
let r be real number ;
cluster r + f -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f + r holds
b1 is continuous
proof end;
cluster f - r -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f - r holds
b1 is continuous ;
cluster r (#) f -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f (#) r holds
b1 is continuous
proof end;
cluster f (/) r -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f (/) r holds
b1 is continuous ;
end;

registration
let T be non empty TopSpace;
let f, g be continuous Function of T,R^1 ;
cluster f + g -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f + g holds
b1 is continuous
proof end;
cluster f - g -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f - g holds
b1 is continuous
proof end;
cluster f (#) g -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f (#) g holds
b1 is continuous
proof end;
end;

registration
let T be non empty TopSpace;
let f be continuous Function of T,R^1 ;
let g be non-empty continuous Function of T,R^1 ;
cluster f /" g -> continuous Function of T,R^1 ;
coherence
for b1 being Function of T,R^1 st b1 = f /" g holds
b1 is continuous
proof end;
end;

registration
let n be Nat;
let T be non empty TopSpace;
let f, g be continuous Function of T,(TOP-REAL n);
cluster f <++> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <++> g holds
b1 is continuous
proof end;
cluster f <--> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <--> g holds
b1 is continuous
proof end;
cluster f <##> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <##> g holds
b1 is continuous
proof end;
end;

registration
let n be Nat;
let T be non empty TopSpace;
let f be continuous Function of T,(TOP-REAL n);
let g be continuous Function of T,R^1 ;
set I = incl g,n;
cluster f <+> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <+> g holds
b1 is continuous
proof end;
cluster f <-> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <-> g holds
b1 is continuous
proof end;
cluster f <#> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f <#> g holds
b1 is continuous
proof end;
end;

registration
let n be Nat;
let T be non empty TopSpace;
let f be continuous Function of T,(TOP-REAL n);
let g be non-empty continuous Function of T,R^1 ;
cluster f </> g -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f </> g holds
b1 is continuous
proof end;
end;

registration
let n be Nat;
let T be non empty TopSpace;
let r be real number ;
let f be continuous Function of T,(TOP-REAL n);
cluster f [+] r -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f [+] r holds
b1 is continuous
proof end;
cluster f [-] r -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f [-] r holds
b1 is continuous ;
cluster f [#] r -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f [#] r holds
b1 is continuous
proof end;
cluster f [/] r -> continuous Function of T,(TOP-REAL n);
coherence
for b1 being Function of T,(TOP-REAL n) st b1 = f [/] r holds
b1 is continuous ;
end;

theorem Th60: :: TOPREALC:60
for r being real non negative number
for n being non zero Nat
for p being Point of (Tcircle (0. (TOP-REAL n)),r) holds - p is Point of (Tcircle (0. (TOP-REAL n)),r)
proof end;

theorem Th61: :: TOPREALC:61
for n being Nat
for r being real non negative number
for f being Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n) holds f (-) is Function of (Tcircle (0. (TOP-REAL (n + 1))),r),(TOP-REAL n)
proof end;

definition
let n be Nat;
let r be real non negative number ;
let X be Subset of (Tcircle (0. (TOP-REAL (n + 1))),r);
:: original: (-)
redefine func (-) X -> Subset of (Tcircle (0. (TOP-REAL (n + 1))),r);
coherence
(-) X is Subset of (Tcircle (0. (TOP-REAL (n + 1))),r)
proof end;
end;

registration
let m be Nat;
let r be real non negative number ;
let X be open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r);
cluster (-) X -> open Subset of (Tcircle (0. (TOP-REAL (m + 1))),r);
coherence
for b1 being Subset of (Tcircle (0. (TOP-REAL (m + 1))),r) st b1 = (-) X holds
b1 is open
proof end;
end;

theorem :: TOPREALC:62
for m being Nat
for r being real non negative number
for f being continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m) holds f (-) is continuous Function of (Tcircle (0. (TOP-REAL (m + 1))),r),(TOP-REAL m)
proof end;