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


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;
cluster r ^2 -> non negative ;
coherence
not r ^2 is negative ;
end;

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

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

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

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

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

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

theorem :: TOPREALC:5
for c being Complex
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
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
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
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
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 holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * |.(r - s).|
proof end;

registration
let f be complex-valued Function;
let x be object ;
let c be Complex;
cluster f +* (x,c) -> complex-valued ;
coherence
f +* (x,c) is complex-valued
proof end;
end;

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

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

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

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

theorem :: TOPREALC:16
for x being object
for n being Nat
for r being Real
for f1 being b2 -element real-valued 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
for g1 being b2 -element complex-valued FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
proof end;

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

theorem :: TOPREALC:19
for f being real-valued FinSequence holds f is FinSequence of REAL by RVSUM_1:145;

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 |.(Sum f).| <= Sum (abs f)
proof end;

theorem :: TOPREALC:22
for A being non empty 1-sorted
for B being 1 -element 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 ;
end;

definition
let n be Nat;
let p be Element of REAL n;
let r be Real;
:: 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
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 by EUCLID:22, EUCLID:77;
end;

registration
cluster TOP-REAL 0 -> trivial ;
coherence
TOP-REAL 0 is trivial ;
end;

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

registration
cluster strict non empty real-functions-membered for 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 TopSpace-like real-functions-membered for 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 for 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 for 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 for 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 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;
:: 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;
:: 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;
:: 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;
:: 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;
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 object ;
let r be Real;
:: 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
for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball (o,r) holds
|.(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 ;
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
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
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
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
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
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
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
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
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 object
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 2;
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 12;
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 n, m being Nat
for r being Real
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;

registration
let T be non empty TopSpace;
cluster Relation-like non-empty the carrier of T -defined the carrier of R^1 -valued Function-like non empty total V18( the carrier of T, the carrier of R^1) complex-valued ext-real-valued real-valued continuous for 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 n, m 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 for 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 for 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;
cluster r + f -> continuous for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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;
let f be continuous Function of T,(TOP-REAL n);
cluster f [+] r -> continuous for 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 for 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 for 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 for 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 non negative Real
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 non negative Real
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 non negative Real;
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 non negative Real;
let X be open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r));
cluster (-) X -> open for 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 non negative Real
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;