:: by Artur Korni{\l}owicz

::

:: Received February 9, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

registration
end;

theorem Th2: :: TOPREALC:2

for c1, c2 being Complex

for f being complex-valued Function holds f (#) (c1 + c2) = (f (#) c1) + (f (#) c2)

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)

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

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

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)

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

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)

for f being complex-valued Function holds (c - d) (#) f = (c (#) f) - (d (#) f)

proof end;

registration

let f be complex-valued Function;

let x be object ;

let c be Complex;

coherence

f +* (x,c) is complex-valued

end;
let x be object ;

let c be Complex;

coherence

f +* (x,c) is complex-valued

proof 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))

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.|

for n being Nat

for r being Real st x in Seg n holds

|.((0* n) +* (x,r)).| = |.r.|

proof end;

theorem Th15: :: TOPREALC:15

for x being object

for n being Nat

for r being Real

for f1 being b_{2} -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))

for n being Nat

for r being Real

for f1 being b

proof end;

theorem :: TOPREALC:16

for x being object

for n being Nat

for r being Real

for f1 being b_{2} -element real-valued FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r

for n being Nat

for r being Real

for f1 being b

proof end;

theorem Th17: :: TOPREALC:17

for i, n being Nat

for c being Complex

for g1 being b_{2} -element complex-valued FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))

for c being Complex

for g1 being b

proof end;

theorem :: TOPREALC:19

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 )

ex i being Nat st

( i in dom f & f . i <> 0 )

proof end;

Lm1: for n being Nat

for f being b

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

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;

coherence

proj (((Seg n) --> T),i) is real-valued

end;
let i be Element of Seg n;

let T be non empty real-membered TopSpace;

coherence

proj (((Seg n) --> T),i) is real-valued

proof 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

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

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

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 ;

end;
attr S is complex-functions-membered means :Def1: :: TOPREALC:def 1

the carrier of S is complex-functions-membered ;

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 ;

the carrier of S is real-functions-membered ;

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

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

for S being 1-sorted holds

( S is real-functions-membered iff the carrier of S is real-functions-membered );

registration

coherence

for b_{1} being 1-sorted st b_{1} is real-functions-membered holds

b_{1} is complex-functions-membered
;

end;
for b

b

registration

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & not b_{1} is empty & b_{1} is real-functions-membered )

end;
ex b

( b

proof end;

registration

let S be complex-functions-membered 1-sorted ;

coherence

the carrier of S is complex-functions-membered by Def1;

end;
coherence

the carrier of S is complex-functions-membered by Def1;

registration

let S be real-functions-membered 1-sorted ;

coherence

the carrier of S is real-functions-membered by Def2;

end;
coherence

the carrier of S is real-functions-membered by Def2;

registration

existence

ex b_{1} being TopSpace st

( b_{1} is strict & not b_{1} is empty & b_{1} is real-functions-membered )

end;
ex b

( b

proof end;

registration

let S be complex-functions-membered TopSpace;

coherence

for b_{1} being SubSpace of S holds b_{1} is complex-functions-membered

end;
coherence

for b

proof end;

registration

let S be real-functions-membered TopSpace;

coherence

for b_{1} being SubSpace of S holds b_{1} is real-functions-membered

end;
coherence

for b

proof end;

definition

let X be complex-functions-membered set ;

ex b_{1} being complex-functions-membered set st

for f being complex-valued Function holds

( - f in b_{1} iff f in X )

for b_{1}, b_{2} being complex-functions-membered set st ( for f being complex-valued Function holds

( - f in b_{1} iff f in X ) ) & ( for f being complex-valued Function holds

( - f in b_{2} iff f in X ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being complex-functions-membered set st ( for f being complex-valued Function holds

( - f in b_{1} iff f in b_{2} ) ) holds

for f being complex-valued Function holds

( - f in b_{2} iff f in b_{1} )

end;
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 for f being complex-valued Function holds

( - f in it iff f in X );

ex b

for f being complex-valued Function holds

( - f in b

proof end;

uniqueness for b

( - f in b

( - f in b

b

proof end;

involutiveness for b

( - f in b

for f being complex-valued Function holds

( - f in b

proof end;

:: deftheorem Def3 defines (-) TOPREALC:def 3 :

for X, b_{2} being complex-functions-membered set holds

( b_{2} = (-) X iff for f being complex-valued Function holds

( - f in b_{2} iff f in X ) );

for X, b

( b

( - f in b

registration
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 )

for f being complex-valued Function holds

( - f in X iff f in (-) X )

proof end;

registration
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)

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

registration

let n be Nat;

let X be open Subset of (TOP-REAL n);

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} = (-) X holds

b_{1} is open

end;
let X be open Subset of (TOP-REAL n);

coherence

for b

b

proof 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

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

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

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

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)

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

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)

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

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)

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

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)

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

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)

for p1, p2 being Point of (TOP-REAL n) holds p1 (#) p2 = p2 (#) p1 ;

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

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)

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

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)

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

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)

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

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

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;

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

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

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)

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)

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)

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)

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;

coherence

f <++> g is FinSequence-like

f <--> g is FinSequence-like

f <##> g is FinSequence-like

f <//> g is FinSequence-like

end;
let f, g be FinSequence of D;

coherence

f <++> g is FinSequence-like

proof end;

coherence f <--> g is FinSequence-like

proof end;

coherence f <##> g is FinSequence-like

proof end;

coherence f <//> g is FinSequence-like

proof 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)

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)

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)

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

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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;

ex b_{1} being Function of T,(TOP-REAL n) st

for t being Element of T holds b_{1} . t = n |-> (f . t)

for b_{1}, b_{2} being Function of T,(TOP-REAL n) st ( for t being Element of T holds b_{1} . t = n |-> (f . t) ) & ( for t being Element of T holds b_{2} . t = n |-> (f . t) ) holds

b_{1} = b_{2}

end;
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 for t being Element of T holds it . t = n |-> (f . t);

ex b

for t being Element of T holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of T,(TOP-REAL n) holds

( b_{5} = incl (f,n) iff for t being Element of T holds b_{5} . t = n |-> (f . t) );

for n being Nat

for T being non empty set

for R being real-membered set

for f being Function of T,R

for b

( b

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

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

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

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

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

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

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;

ex b_{1} being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st

for x, y being Point of (TOP-REAL n) holds b_{1} . (x,y) = x (#) y

for b_{1}, b_{2} being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) st ( for x, y being Point of (TOP-REAL n) holds b_{1} . (x,y) = x (#) y ) & ( for x, y being Point of (TOP-REAL n) holds b_{2} . (x,y) = x (#) y ) holds

b_{1} = b_{2}

end;
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 for x, y being Point of (TOP-REAL n) holds it . (x,y) = x (#) y;

ex b

for x, y being Point of (TOP-REAL n) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines TIMES TOPREALC:def 5 :

for n being Nat

for b_{2} being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) holds

( b_{2} = TIMES n iff for x, y being Point of (TOP-REAL n) holds b_{2} . (x,y) = x (#) y );

for n being Nat

for b

( b

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)

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;

ex b_{1} being Function of (TOP-REAL m),R^1 st

for p being Element of (TOP-REAL m) holds b_{1} . p = p /. n
by A1, JORDAN2B:1;

uniqueness

for b_{1}, b_{2} being Function of (TOP-REAL m),R^1 st ( for p being Element of (TOP-REAL m) holds b_{1} . p = p /. n ) & ( for p being Element of (TOP-REAL m) holds b_{2} . p = p /. n ) holds

b_{1} = b_{2}

end;
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 for p being Element of (TOP-REAL m) holds it . p = p /. n;

ex b

for p being Element of (TOP-REAL m) holds b

uniqueness

for b

b

proof end;

:: deftheorem Def6 defines PROJ TOPREALC:def 6 :

for m, n being Nat

for b_{3} being Function of (TOP-REAL m),R^1 holds

( b_{3} = PROJ (m,n) iff for p being Element of (TOP-REAL m) holds b_{3} . p = p /. n );

for m, n being Nat

for b

( b

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).[

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

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;

ex b_{1} being Function of T,R^1 st

( b_{1} is non-empty & b_{1} is continuous )

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

( b

proof end;

registration

let n be Nat;

let T be non empty TopSpace;

let f be continuous Function of T,R^1;

coherence

incl (f,n) is continuous

end;
let T be non empty TopSpace;

let f be continuous Function of T,R^1;

coherence

incl (f,n) is continuous

proof end;

registration
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)

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;

coherence

for b_{1} being Function of T,R^1 st b_{1} = - f holds

b_{1} is continuous

end;
let f be continuous Function of T,R^1;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be non-empty continuous Function of T,R^1;

coherence

for b_{1} being Function of T,R^1 st b_{1} = f " holds

b_{1} is continuous

end;
let f be non-empty continuous Function of T,R^1;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous Function of T,R^1;

let r be Real;

coherence

for b_{1} being Function of T,R^1 st b_{1} = f + r holds

b_{1} is continuous

for b_{1} being Function of T,R^1 st b_{1} = f - r holds

b_{1} is continuous
;

coherence

for b_{1} being Function of T,R^1 st b_{1} = f (#) r holds

b_{1} is continuous

for b_{1} being Function of T,R^1 st b_{1} = f (/) r holds

b_{1} is continuous
;

end;
let f be continuous Function of T,R^1;

let r be Real;

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

proof end;

coherence for b

b

registration

let T be non empty TopSpace;

let f, g be continuous Function of T,R^1;

coherence

for b_{1} being Function of T,R^1 st b_{1} = f + g holds

b_{1} is continuous

for b_{1} being Function of T,R^1 st b_{1} = f - g holds

b_{1} is continuous

for b_{1} being Function of T,R^1 st b_{1} = f (#) g holds

b_{1} is continuous

end;
let f, g be continuous Function of T,R^1;

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

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

coherence

for b_{1} being Function of T,R^1 st b_{1} = f /" g holds

b_{1} is continuous

end;
let f be continuous Function of T,R^1;

let g be non-empty continuous Function of T,R^1;

coherence

for b

b

proof end;

registration

let n be Nat;

let T be non empty TopSpace;

let f, g be continuous Function of T,(TOP-REAL n);

coherence

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <++> g holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <--> g holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <##> g holds

b_{1} is continuous

end;
let T be non empty TopSpace;

let f, g be continuous Function of T,(TOP-REAL n);

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

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

coherence

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <+> g holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <-> g holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f <#> g holds

b_{1} is continuous

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

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

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

coherence

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f </> g holds

b_{1} is continuous

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

coherence

for b

b

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

coherence

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f [+] r holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f [-] r holds

b_{1} is continuous
;

coherence

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f [#] r holds

b_{1} is continuous

for b_{1} being Function of T,(TOP-REAL n) st b_{1} = f [/] r holds

b_{1} is continuous
;

end;
let T be non empty TopSpace;

let r be Real;

let f be continuous Function of T,(TOP-REAL n);

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

proof end;

coherence for b

b

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

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)

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

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

registration

let m be Nat;

let r be non negative Real;

let X be open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r));

coherence

for b_{1} being Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st b_{1} = (-) X holds

b_{1} is open

end;
let r be non negative Real;

let X be open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r));

coherence

for b

b

proof 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)

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;