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


begin

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

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

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

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

registration
let f be empty set ;
clusterf ^2  ->  empty ;
coherence
 sqr f is empty ;
cluster|.f.| ->  zero ;
coherence
 |.f.| is empty by RVSUM_1:72;
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)
proofend;

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

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

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

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

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
proofend;

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

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

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

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

registration
let f be complex-valued Function;
let x be set ;
let c be complex number ;
clusterf +* (x,c) ->  complex-valued ;
coherence
 f +* (x,c) is complex-valued
proofend;
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))
proofend;

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
proofend;

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

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

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

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

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

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 &amp; f . i <> 0 )
proofend;

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

Lm1:  for n being Nat
for f being real-valued b1 -element FinSequence holds f is Element of n -tuples_on REAL
proofend;

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
proofend;

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
proofend;
end;

definition
let n be Nat;
let p be Element of REAL n;
let r be real number ;
:: original:(/)
redefine funcp (/) r ->  Element of REAL n;
coherence
 p (/) r is Element of REAL n
proofend;
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) )
proofend;

definition
let S be 1-sorted ;
attrS is complex-functions-membered  means :Def1: :: TOPREALC:def 1
 the carrier of S is complex-functions-membered ;
attrS 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
proofend;
end;

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

registration
cluster TOP-REAL 0 ->  trivial ;
coherence
 TOP-REAL 0 is trivial by EUCLID:22, EUCLID:77;
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
proofend;
end;

registration
cluster strict non empty real-functions-membered for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is strict &amp; not b1 is empty &amp; b1 is real-functions-membered )
proofend;
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 &amp; not b1 is empty &amp; b1 is real-functions-membered )
proofend;
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
proofend;
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
proofend;
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 )
proofend;
uniqueness
 for b1, b2 being complex-functions-membered set st ( for f being complex-valued Function holds
( - f in b1 iff f in X ) ) &amp; ( for f being complex-valued Function holds
( - f in b2 iff f in X ) ) holds
b1 = b2
proofend;
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 )
proofend;
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
proofend;
end;

registration
let X be non empty complex-functions-membered set ;
cluster (-) X ->  non empty complex-functions-membered ;
coherence
 not (-) X is empty
proofend;
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 )
proofend;

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

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

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)
proofend;
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
proofend;
end;

definition
let n be Nat;
let p be Element of (TOP-REAL n);
let x be set ;
:: original:.
redefine funcp . 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 funcf . x ->  Point of T;
coherence
 f . x is Point of T
proofend;
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 funcf . (r,s) ->  Point of T;
coherence
 f . (r,s) is Point of T
proofend;
end;

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

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

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

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

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original:(#)
redefine funcp1 (#) p2 ->  Point of (TOP-REAL n);
coherence
 p1 (#) p2 is Point of (TOP-REAL n)
proofend;
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)
proofend;
end;

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original:/"
redefine funcp1 /" p2 ->  Point of (TOP-REAL n);
coherence
 p1 /" p2 is Point of (TOP-REAL n)
proofend;
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 funcp +* (x,r) ->  Point of (TOP-REAL n);
coherence
 p +* (x,r) is Point of (TOP-REAL n)
proofend;
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 &amp; a in Ball (o,r) holds
abs (Sum (a - o)) < n * r
proofend;

registration
let n be Nat;
cluster Euclid n ->  real-functions-membered ;
coherence
 Euclid n is real-functions-membered
proofend;
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
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

registration
let D be complex-functions-membered set ;
let f, g be FinSequence of D;
clusterf <++> g ->  FinSequence-like ;
coherence
 f <++> g is FinSequence-like
proofend;
clusterf <--> g ->  FinSequence-like ;
coherence
 f <--> g is FinSequence-like
proofend;
clusterf <##> g ->  FinSequence-like ;
coherence
 f <##> g is FinSequence-like
proofend;
clusterf <//> g ->  FinSequence-like ;
coherence
 f <//> g is FinSequence-like
proofend;
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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;
uniqueness
 for b1, b2 being Function of T,(TOP-REAL n) st ( for t being Element of T holds b1 . t = n |-> (f . t) ) &amp; ( for t being Element of T holds b2 . t = n |-> (f . t) ) holds
b1 = b2
proofend;
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
proofend;

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
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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
proofend;
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 ) &amp; ( for x, y being Point of (TOP-REAL n) holds b2 . (x,y) = x (#) y ) holds
b1 = b2
proofend;
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))
proofend;

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)
proofend;

definition
let m, n be Nat;
A1: ( m in NAT &amp; 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 ) &amp; ( for p being Element of (TOP-REAL m) holds b2 . p = p /. n ) holds
b1 = b2
proofend;
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).[
proofend;

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))
proofend;

begin

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 &amp; b1 is continuous )
proofend;
end;

theorem :: TOPREALC:57
for n, m being Nat st n in Seg m holds
PROJ (m,n) is continuous
proofend;

theorem :: TOPREALC:58
for n, m being Nat st n in Seg m holds
PROJ (m,n) is open
proofend;

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
proofend;
end;

registration
let n be Nat;
cluster TIMES n ->  continuous ;
coherence
 TIMES n is continuous
proofend;
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)
proofend;

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
proofend;
end;

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

registration
let T be non empty TopSpace;
let f be continuous Function of T,R^1;
let r be real number ;
clusterr + 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
proofend;
clusterf - 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 ;
clusterr (#) 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
proofend;
clusterf (/) 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;
clusterf + 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
proofend;
clusterf - 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
proofend;
clusterf (#) 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
proofend;
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;
clusterf /" 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
proofend;
end;

registration
let n be Nat;
let T be non empty TopSpace;
let f, g be continuous Function of T,(TOP-REAL n);
clusterf <++> 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
proofend;
clusterf <--> 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
proofend;
clusterf <##> 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
proofend;
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);
clusterf <+> 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
proofend;
clusterf <-> 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
proofend;
clusterf <#> 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
proofend;
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;
clusterf </> 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
proofend;
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);
clusterf [+] 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
proofend;
clusterf [-] 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 ;
clusterf [#] 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
proofend;
clusterf [/] 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 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))
proofend;

theorem Th61: :: TOPREALC:61
for n being Nat
for r being non negative real 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)
proofend;

definition
let n be Nat;
let r be non negative real 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))
proofend;
end;

registration
let m be Nat;
let r be non negative real number ;
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
proofend;
end;

theorem :: TOPREALC:62
for m being Nat
for r being non negative real 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)
proofend;