:: TOPREALC semantic presentation

begin


theorem :: TOPREALC:1
for X being trivial set
for Y being set st X,Y are_equipotent holds
Y is trivial
proof
let X be trivial set ; ::_thesis: for Y being set st X,Y are_equipotent holds
Y is trivial
let Y be set ; ::_thesis: ( X,Y are_equipotent implies Y is trivial )
assume A1: X,Y are_equipotent ; ::_thesis: Y is trivial
A2: card X < 2 by NAT_D:60;
A3: Y is finite by A1, CARD_1:38;
 card X = card Y by A1, CARD_1:5;
hence  Y is trivial by A2, A3, NAT_D:60; ::_thesis: verum
end;

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)
proof
let c1, c2 be complex number ; ::_thesis: for f being complex-valued Function holds f (#) (c1 + c2) = (f (#) c1) + (f (#) c2)
let f be complex-valued Function; ::_thesis: f (#) (c1 + c2) = (f (#) c1) + (f (#) c2)
A1: dom (f (#) (c1 + c2)) = dom f by VALUED_1:def_5;
A2: dom (f (#) c1) = dom f by VALUED_1:def_5;
A3: dom (f (#) c2) = dom f by VALUED_1:def_5;
A4: dom ((f (#) c1) + (f (#) c2)) = (dom (f (#) c1)) /\ (dom (f (#) c2)) by VALUED_1:def_1;
hence  dom (f (#) (c1 + c2)) = dom ((f (#) c1) + (f (#) c2)) by A2, A3, VALUED_1:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom (f (#) (c1 + c2)) or (f (#) (c1 + c2)) . b1 = ((f (#) c1) + (f (#) c2)) . b1 )
let x be set ; ::_thesis: ( not x in dom (f (#) (c1 + c2)) or (f (#) (c1 + c2)) . x = ((f (#) c1) + (f (#) c2)) . x )
assume A5: x in dom (f (#) (c1 + c2)) ; ::_thesis: (f (#) (c1 + c2)) . x = ((f (#) c1) + (f (#) c2)) . x
hence (f (#) (c1 + c2)) . x = (f . x) * (c1 + c2) by VALUED_1:def_5
.= ((f . x) * c1) + ((f . x) * c2)
.= ((f (#) c1) . x) + ((f . x) * c2) by A1, A2, A5, VALUED_1:def_5
.= ((f (#) c1) . x) + ((f (#) c2) . x) by A1, A3, A5, VALUED_1:def_5
.= ((f (#) c1) + (f (#) c2)) . x by A1, A2, A3, A4, A5, VALUED_1:def_1 ;
::_thesis: verum
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
let c1, c2 be complex number ; ::_thesis: for f being complex-valued Function holds f (#) (c1 - c2) = (f (#) c1) - (f (#) c2)
let f be complex-valued Function; ::_thesis: f (#) (c1 - c2) = (f (#) c1) - (f (#) c2)
thus f (#) (c1 - c2) = (f (#) c1) + (f (#) (- c2)) by Th2
.= (f (#) c1) - (f (#) c2) by VALUED_2:24 ; ::_thesis: verum
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
let c be complex number ; ::_thesis: for f, g being complex-valued Function holds (f (/) c) + (g (/) c) = (f + g) (/) c
let f, g be complex-valued Function; ::_thesis: (f (/) c) + (g (/) c) = (f + g) (/) c
A1: dom ((f (/) c) + (g (/) c)) = (dom (f (/) c)) /\ (dom (g (/) c)) by VALUED_1:def_1;
A2: dom (f (/) c) = dom f by VALUED_2:28;
A3: dom (g (/) c) = dom g by VALUED_2:28;
A4: dom ((f + g) (/) c) = dom (f + g) by VALUED_2:28;
A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
thus  dom ((f (/) c) + (g (/) c)) = dom ((f + g) (/) c) by A1, A2, A3, A4, VALUED_1:def_1; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f (/) c) + (g (/) c)) or ((f (/) c) + (g (/) c)) . b1 = ((f + g) (/) c) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f (/) c) + (g (/) c)) or ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x )
assume A6: x in dom ((f (/) c) + (g (/) c)) ; ::_thesis: ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x
thus ((f + g) (/) c) . x = ((f + g) . x) / c by VALUED_2:29
.= ((f . x) + (g . x)) / c by A1, A2, A3, A6, A5, VALUED_1:def_1
.= ((f . x) / c) + ((g . x) / c)
.= ((f . x) / c) + ((g (/) c) . x) by VALUED_2:29
.= ((f (/) c) . x) + ((g (/) c) . x) by VALUED_2:29
.= ((f (/) c) + (g (/) c)) . x by A6, VALUED_1:def_1 ; ::_thesis: verum
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
let c be complex number ; ::_thesis: for f, g being complex-valued Function holds (f (/) c) - (g (/) c) = (f - g) (/) c
let f, g be complex-valued Function; ::_thesis: (f (/) c) - (g (/) c) = (f - g) (/) c
thus (f (/) c) - (g (/) c) = (f (/) c) + ((- g) (/) c) by VALUED_2:30
.= (f - g) (/) c by Th4 ; ::_thesis: verum
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
let c1, c2 be complex number ; ::_thesis: for f, g being complex-valued Function st c1 <> 0 & c2 <> 0 holds
(f (/) c1) - (g (/) c2) = ((f (#) c2) - (g (#) c1)) (/) (c1 * c2)
let f, g be complex-valued Function; ::_thesis: ( c1 <> 0 & c2 <> 0 implies (f (/) c1) - (g (/) c2) = ((f (#) c2) - (g (#) c1)) (/) (c1 * c2) )
assume A1: ( c1 <> 0 & c2 <> 0 ) ; ::_thesis: (f (/) c1) - (g (/) c2) = ((f (#) c2) - (g (#) c1)) (/) (c1 * c2)
A2: dom (f (/) c1) = dom f by VALUED_2:28;
A3: dom (g (/) c2) = dom g by VALUED_2:28;
A4: dom (f (#) c2) = dom f by VALUED_1:def_5;
A5: dom (g (#) c1) = dom g by VALUED_1:def_5;
A6: dom ((f (/) c1) - (g (/) c2)) = (dom (f (/) c1)) /\ (dom (g (/) c2)) by VALUED_1:12;
A7: dom ((f (#) c2) - (g (#) c1)) = (dom (f (#) c2)) /\ (dom (g (#) c1)) by VALUED_1:12;
hence  dom ((f (/) c1) - (g (/) c2)) = dom (((f (#) c2) - (g (#) c1)) (/) (c1 * c2)) by A2, A3, A4, A5, A6, VALUED_2:28; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f (/) c1) - (g (/) c2)) or ((f (/) c1) - (g (/) c2)) . b1 = (((f (#) c2) - (g (#) c1)) (/) (c1 * c2)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f (/) c1) - (g (/) c2)) or ((f (/) c1) - (g (/) c2)) . x = (((f (#) c2) - (g (#) c1)) (/) (c1 * c2)) . x )
assume A8: x in dom ((f (/) c1) - (g (/) c2)) ; ::_thesis: ((f (/) c1) - (g (/) c2)) . x = (((f (#) c2) - (g (#) c1)) (/) (c1 * c2)) . x
hence ((f (/) c1) - (g (/) c2)) . x = ((f (/) c1) . x) - ((g (/) c2) . x) by VALUED_1:13
.= ((f . x) / c1) - ((g (/) c2) . x) by VALUED_2:29
.= ((f . x) / c1) - ((g . x) / c2) by VALUED_2:29
.= (((f . x) * c2) - ((g . x) * c1)) / (c1 * c2) by A1, XCMPLX_1:130
.= (((f . x) * c2) - ((g (#) c1) . x)) / (c1 * c2) by VALUED_1:6
.= (((f (#) c2) . x) - ((g (#) c1) . x)) / (c1 * c2) by VALUED_1:6
.= (((f (#) c2) - (g (#) c1)) . x) / (c1 * c2) by A2, A3, A4, A5, A6, A7, A8, VALUED_1:13
.= (((f (#) c2) - (g (#) c1)) (/) (c1 * c2)) . x by VALUED_2:29 ;
::_thesis: verum
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
let c be complex number ; ::_thesis: for f, g being complex-valued Function st c <> 0 holds
(f (/) c) - g = (f - (c (#) g)) (/) c
let f, g be complex-valued Function; ::_thesis: ( c <> 0 implies (f (/) c) - g = (f - (c (#) g)) (/) c )
assume A1: c <> 0 ; ::_thesis: (f (/) c) - g = (f - (c (#) g)) (/) c
A2: dom ((f (/) c) - g) = (dom (f (/) c)) /\ (dom g) by VALUED_1:12
.= (dom f) /\ (dom g) by VALUED_2:28 ;
A3: dom (f - (c (#) g)) = (dom f) /\ (dom (c (#) g)) by VALUED_1:12
.= (dom f) /\ (dom g) by VALUED_1:def_5 ;
hence  dom ((f (/) c) - g) = dom ((f - (c (#) g)) (/) c) by A2, VALUED_2:28; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f (/) c) - g) or ((f (/) c) - g) . b1 = ((f - (c (#) g)) (/) c) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f (/) c) - g) or ((f (/) c) - g) . x = ((f - (c (#) g)) (/) c) . x )
assume A4: x in dom ((f (/) c) - g) ; ::_thesis: ((f (/) c) - g) . x = ((f - (c (#) g)) (/) c) . x
hence ((f (/) c) - g) . x = ((f (/) c) . x) - (g . x) by VALUED_1:13
.= ((f . x) / c) - (g . x) by VALUED_2:29
.= ((f . x) / c) - ((c * (g . x)) / c) by A1, XCMPLX_1:89
.= ((f . x) / c) - (((c (#) g) . x) / c) by VALUED_1:6
.= ((f . x) - ((c (#) g) . x)) / c
.= ((f - (c (#) g)) . x) / c by A2, A3, A4, VALUED_1:13
.= ((f - (c (#) g)) (/) c) . x by VALUED_2:29 ;
::_thesis: verum
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
let c, d be complex number ; ::_thesis: for f being complex-valued Function holds (c - d) (#) f = (c (#) f) - (d (#) f)
let f be complex-valued Function; ::_thesis: (c - d) (#) f = (c (#) f) - (d (#) f)
dom ((c (#) f) - (d (#) f)) = (dom (c (#) f)) /\ (dom (d (#) f)) by VALUED_1:12
.= (dom f) /\ (dom (d (#) f)) by VALUED_1:def_5
.= (dom f) /\ (dom f) by VALUED_1:def_5 ;
hence A1: dom ((c - d) (#) f) = dom ((c (#) f) - (d (#) f)) by VALUED_1:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((c - d) (#) f) or ((c - d) (#) f) . b1 = ((c (#) f) - (d (#) f)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((c - d) (#) f) or ((c - d) (#) f) . x = ((c (#) f) - (d (#) f)) . x )
assume A2: x in dom ((c - d) (#) f) ; ::_thesis: ((c - d) (#) f) . x = ((c (#) f) - (d (#) f)) . x
thus ((c - d) (#) f) . x = (c - d) * (f . x) by VALUED_1:6
.= (c * (f . x)) - (d * (f . x))
.= (c * (f . x)) - ((d (#) f) . x) by VALUED_1:6
.= ((c (#) f) . x) - ((d (#) f) . x) by VALUED_1:6
.= ((c (#) f) - (d (#) f)) . x by A1, A2, VALUED_1:13 ; ::_thesis: verum
end;

theorem :: TOPREALC:9
for f, g being complex-valued Function holds (f - g) ^2 = (g - f) ^2
proof
let f, g be complex-valued Function; ::_thesis: (f - g) ^2 = (g - f) ^2
A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
A2: dom (g - f) = (dom g) /\ (dom f) by VALUED_1:12;
A3: dom ((f - g) ^2) = dom (f - g) by VALUED_1:11;
hence  dom ((f - g) ^2) = dom ((g - f) ^2) by A1, A2, VALUED_1:11; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f - g) ^2) or ((f - g) ^2) . b1 = ((g - f) ^2) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f - g) ^2) or ((f - g) ^2) . x = ((g - f) ^2) . x )
assume A4: x in dom ((f - g) ^2) ; ::_thesis: ((f - g) ^2) . x = ((g - f) ^2) . x
then A5: (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;
A6: (g - f) . x = (g . x) - (f . x) by A1, A3, A4, A2, VALUED_1:13;
thus ((f - g) ^2) . x = ((f - g) . x) * ((f - g) . x) by VALUED_1:5
.= ((g - f) . x) * ((g - f) . x) by A5, A6
.= ((g - f) ^2) . x by VALUED_1:5 ; ::_thesis: verum
end;

theorem :: TOPREALC:10
for c being complex number
for f being complex-valued Function holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
proof
let c be complex number ; ::_thesis: for f being complex-valued Function holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
let f be complex-valued Function; ::_thesis: (f (/) c) ^2 = (f ^2) (/) (c ^2)
thus  dom ((f (/) c) ^2) = dom (f (/) c) by VALUED_1:11
.= dom f by VALUED_2:28
.= dom (f ^2) by VALUED_1:11
.= dom ((f ^2) (/) (c ^2)) by VALUED_2:28 ; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f (/) c) ^2) or ((f (/) c) ^2) . b1 = ((f ^2) (/) (c ^2)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f (/) c) ^2) or ((f (/) c) ^2) . x = ((f ^2) (/) (c ^2)) . x )
assume  x in dom ((f (/) c) ^2) ; ::_thesis: ((f (/) c) ^2) . x = ((f ^2) (/) (c ^2)) . x
thus ((f (/) c) ^2) . x = ((f (/) c) . x) ^2 by VALUED_1:11
.= ((f . x) / c) ^2 by VALUED_2:29
.= ((f . x) ^2) / (c ^2) by XCMPLX_1:76
.= ((f ^2) . x) / (c ^2) by VALUED_1:11
.= ((f ^2) (/) (c ^2)) . x by VALUED_2:29 ; ::_thesis: verum
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
let n be Nat; ::_thesis: for r, s being real number holds |.((n |-> r) - (n |-> s)).| = (sqrt n) * (abs (r - s))
let r, s be real number ; ::_thesis: |.((n |-> r) - (n |-> s)).| = (sqrt n) * (abs (r - s))
thus |.((n |-> r) - (n |-> s)).| = sqrt (Sum (sqr (n |-> (r - s)))) by RVSUM_1:30
.= sqrt (Sum (n |-> ((r - s) ^2))) by RVSUM_1:56
.= sqrt (n * ((r - s) ^2)) by RVSUM_1:80
.= (sqrt n) * (sqrt ((r - s) ^2)) by SQUARE_1:29
.= (sqrt n) * (abs (r - s)) by COMPLEX1:72 ; ::_thesis: verum
end;

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
proof
set F = f +* (x,c);
let a be set ; :: according to VALUED_0:def_7 ::_thesis: ( not a in dom (f +* (x,c)) or (f +* (x,c)) . a is complex )
assume  a in dom (f +* (x,c)) ; ::_thesis: (f +* (x,c)) . a is complex
percases ( ( x in dom f & x = a ) or ( x in dom f & x <> a ) or not x in dom f ) ;
suppose ( x in dom f & x = a ) ; ::_thesis: (f +* (x,c)) . a is complex
hence  (f +* (x,c)) . a is complex by FUNCT_7:31; ::_thesis: verum
end;
suppose ( x in dom f & x <> a ) ; ::_thesis: (f +* (x,c)) . a is complex
then  (f +* (x,c)) . a = f . a by FUNCT_7:32;
hence  (f +* (x,c)) . a is complex ; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: (f +* (x,c)) . a is complex
then  (f +* (x,c)) . a = f . a by FUNCT_7:def_3;
hence  (f +* (x,c)) . a is complex ; ::_thesis: verum
end;
end;
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
let x be set ; ::_thesis: for n being Nat
for c being complex number holds ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
let n be Nat; ::_thesis: for c being complex number holds ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
let c be complex number ; ::_thesis: ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))
set f = (0* n) +* (x,c);
set g = (0* n) +* (x,(c ^2));
A1: dom ((0* n) +* (x,c)) = dom (0* n) by FUNCT_7:30;
A2: dom ((0* n) +* (x,(c ^2))) = dom (0* n) by FUNCT_7:30;
A3: dom (((0* n) +* (x,c)) ^2) = dom ((0* n) +* (x,c)) by VALUED_1:11;
thus  dom (((0* n) +* (x,c)) ^2) = dom ((0* n) +* (x,(c ^2))) by A1, A2, VALUED_1:11; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom (((0* n) +* (x,c)) ^2) or (((0* n) +* (x,c)) ^2) . b1 = ((0* n) +* (x,(c ^2))) . b1 )
let a be set ; ::_thesis: ( not a in dom (((0* n) +* (x,c)) ^2) or (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a )
assume A4: a in dom (((0* n) +* (x,c)) ^2) ; ::_thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
A5: (((0* n) +* (x,c)) ^2) . a = (((0* n) +* (x,c)) . a) ^2 by VALUED_1:11;
percases ( a = x or a <> x ) ;
supposeA6: a = x ; ::_thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
then  ((0* n) +* (x,c)) . a = c by A1, A3, A4, FUNCT_7:31;
hence  (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a by A6, A1, A3, A4, A5, FUNCT_7:31; ::_thesis: verum
end;
supposeA7: a <> x ; ::_thesis: (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a
then A8: ((0* n) +* (x,c)) . a = (n |-> 0) . a by FUNCT_7:32
.= {} . x ;
((0* n) +* (x,(c ^2))) . a = (n |-> 0) . a by A7, FUNCT_7:32
.= {} . x ;
hence  (((0* n) +* (x,c)) ^2) . a = ((0* n) +* (x,(c ^2))) . a by A5, A8; ::_thesis: verum
end;
end;
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
let x be set ; ::_thesis: for n being Nat
for r being real number st x in Seg n holds
|.((0* n) +* (x,r)).| = abs r
let n be Nat; ::_thesis: for r being real number st x in Seg n holds
|.((0* n) +* (x,r)).| = abs r
let r be real number ; ::_thesis: ( x in Seg n implies |.((0* n) +* (x,r)).| = abs r )
set f = (0* n) +* (x,r);
A1: r ^2 in REAL by XREAL_0:def_1;
A2: n in NAT by ORDINAL1:def_12;
assume A3: x in Seg n ; ::_thesis: |.((0* n) +* (x,r)).| = abs r
 ((0* n) +* (x,r)) ^2 = (0* n) +* (x,(r ^2)) by Th12;
then  Sum (((0* n) +* (x,r)) ^2) = r ^2 by A3, A1, A2, JORDAN2B:10;
hence  |.((0* n) +* (x,r)).| = abs r by COMPLEX1:72; ::_thesis: verum
end;

theorem Th14: :: TOPREALC:14
for x being set
for n being Nat holds (0.REAL n) +* (x,0) = 0.REAL n
proof
let x be set ; ::_thesis: for n being Nat holds (0.REAL n) +* (x,0) = 0.REAL n
let n be Nat; ::_thesis: (0.REAL n) +* (x,0) = 0.REAL n
set p = (0.REAL n) +* (x,0);
A1: dom ((0.REAL n) +* (x,0)) = Seg n by FINSEQ_1:89;
A2: dom ((0.REAL n) +* (x,0)) = dom (0.REAL n) by FUNCT_7:30;
A3: dom (0.REAL n) = Seg n by FINSEQ_1:89;
now__::_thesis:_for_z_being_set_st_z_in_dom_((0.REAL_n)_+*_(x,0))_holds_
((0.REAL_n)_+*_(x,0))_._z_=_(0.REAL_n)_._z
let z be set ; ::_thesis: ( z in dom ((0.REAL n) +* (x,0)) implies ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1 )
assume A4: z in dom ((0.REAL n) +* (x,0)) ; ::_thesis: ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1
percases ( z = x or z <> x ) ;
suppose z = x ; ::_thesis: ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1
hence ((0.REAL n) +* (x,0)) . z = 0 by A1, A3, A4, FUNCT_7:31
.= (0.REAL n) . z ;
::_thesis: verum
end;
suppose z <> x ; ::_thesis: ((0.REAL n) +* (x,0)) . b1 = (0.REAL n) . b1
hence  ((0.REAL n) +* (x,0)) . z = (0.REAL n) . z by FUNCT_7:32; ::_thesis: verum
end;
end;
end;
hence  (0.REAL n) +* (x,0) = 0.REAL n by A2, FUNCT_1:2; ::_thesis: verum
end;

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))
proof
let x be set ; ::_thesis: for n being Nat
for r being real number
for f1 being real-valued b1 -element FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let n be Nat; ::_thesis: for r being real number
for f1 being real-valued n -element FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let r be real number ; ::_thesis: for f1 being real-valued n -element FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
let f1 be real-valued n -element FinSequence; ::_thesis: mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))
set p = (0.REAL n) +* (x,r);
A1: dom f1 = Seg n by FINSEQ_1:89;
A2: dom ((0.REAL n) +* (x,r)) = Seg n by FINSEQ_1:89;
A3: dom (mlt (f1,((0.REAL n) +* (x,r)))) = (dom f1) /\ (dom ((0.REAL n) +* (x,r))) by VALUED_1:def_4;
A4: dom ((0.REAL n) +* (x,((f1 . x) * r))) = dom (0.REAL n) by FUNCT_7:30;
A5: dom (0.REAL n) = Seg n by FINSEQ_1:89;
now__::_thesis:_for_z_being_set_st_z_in_dom_(mlt_(f1,((0.REAL_n)_+*_(x,r))))_holds_
(mlt_(f1,((0.REAL_n)_+*_(x,r))))_._z_=_((0.REAL_n)_+*_(x,((f1_._x)_*_r)))_._z
let z be set ; ::_thesis: ( z in dom (mlt (f1,((0.REAL n) +* (x,r)))) implies (mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1 )
assume A6: z in dom (mlt (f1,((0.REAL n) +* (x,r)))) ; ::_thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1
A7: (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * (((0.REAL n) +* (x,r)) . z) by VALUED_1:5;
percases ( z = x or z <> x ) ;
supposeA8: z = x ; ::_thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1
hence (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * r by A1, A2, A3, A5, A6, A7, FUNCT_7:31
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A1, A2, A3, A5, A6, A8, FUNCT_7:31 ;
::_thesis: verum
end;
supposeA9: z <> x ; ::_thesis: (mlt (f1,((0.REAL n) +* (x,r)))) . b1 = ((0.REAL n) +* (x,((f1 . x) * r))) . b1
hence (mlt (f1,((0.REAL n) +* (x,r)))) . z = (f1 . z) * ((0.REAL n) . z) by A7, FUNCT_7:32
.= (f1 . z) * ((n |-> 0) . z)
.= ((0.REAL n) +* (x,((f1 . x) * r))) . z by A9, FUNCT_7:32 ;
::_thesis: verum
end;
end;
end;
hence  mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r)) by A4, A5, FINSEQ_1:89, FUNCT_1:2; ::_thesis: verum
end;

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
proof
let x be set ; ::_thesis: for n being Nat
for r being real number
for f1 being real-valued b1 -element FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let n be Nat; ::_thesis: for r being real number
for f1 being real-valued n -element FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let r be real number ; ::_thesis: for f1 being real-valued n -element FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
let f1 be real-valued n -element FinSequence; ::_thesis: |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
A1: mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r)) by Th15;
A2: dom f1 = Seg n by FINSEQ_1:89;
A3: n in NAT by ORDINAL1:def_12;
A4: (f1 . x) * r in REAL by XREAL_0:def_1;
percases ( x in dom f1 or not x in dom f1 ) ;
suppose x in dom f1 ; ::_thesis: |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
hence  |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r by A1, A2, A3, A4, JORDAN2B:10; ::_thesis: verum
end;
suppose not x in dom f1 ; ::_thesis: |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r
then A5: f1 . x = 0 by FUNCT_1:def_2;
hence |(f1,((0.REAL n) +* (x,r)))| = Sum (0.REAL n) by A1, Th14
.= (f1 . x) * r by A5, A3, JORDAN2B:9 ;
::_thesis: verum
end;
end;
end;

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)))
proof
let i, n be Nat; ::_thesis: for c being complex number
for g1 being complex-valued n -element FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let c be complex number ; ::_thesis: for g1 being complex-valued n -element FinSequence holds (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
let g1 be complex-valued n -element FinSequence; ::_thesis: (g1 +* (i,c)) - g1 = (0* n) +* (i,(c - (g1 . i)))
A1: dom ((g1 +* (i,c)) - g1) = (dom (g1 +* (i,c))) /\ (dom g1) by VALUED_1:12;
A2: dom (0* n) = Seg n by FINSEQ_1:89;
A3: dom g1 = Seg n by FINSEQ_1:89;
A4: dom (g1 +* (i,c)) = dom g1 by FUNCT_7:30;
hence  dom ((g1 +* (i,c)) - g1) = dom ((0* n) +* (i,(c - (g1 . i)))) by A1, A3, FINSEQ_1:89; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . b1 = ((0* n) +* (i,(c - (g1 . i)))) . b1 )
let x be set ; ::_thesis: ( not x in dom ((g1 +* (i,c)) - g1) or ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x )
assume A5: x in dom ((g1 +* (i,c)) - g1) ; ::_thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x
then A6: ((g1 +* (i,c)) - g1) . x = ((g1 +* (i,c)) . x) - (g1 . x) by VALUED_1:13;
percases ( x = i or x <> i ) ;
supposeA7: x = i ; ::_thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x
hence ((g1 +* (i,c)) - g1) . x = c - (g1 . x) by A6, A1, A5, A4, FUNCT_7:31
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A1, A2, A3, A5, A4, A7, FUNCT_7:31 ;
::_thesis: verum
end;
supposeA8: x <> i ; ::_thesis: ((g1 +* (i,c)) - g1) . x = ((0* n) +* (i,(c - (g1 . i)))) . x
hence ((g1 +* (i,c)) - g1) . x = (g1 . x) - (g1 . x) by A6, FUNCT_7:32
.= (n |-> 0) . x
.= ((0* n) +* (i,(c - (g1 . i)))) . x by A8, FUNCT_7:32 ;
::_thesis: verum
end;
end;
end;

theorem :: TOPREALC:18
for r being real number holds |.<*r*>.| = abs r
proof
let r be real number ; ::_thesis: |.<*r*>.| = abs r
set f = <*r*>;
 sqr <*r*> = <*(r ^2)*> by RVSUM_1:55;
then  Sum (sqr <*r*>) = r ^2 by RVSUM_1:73;
hence  |.<*r*>.| = abs r by COMPLEX1:72; ::_thesis: verum
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
let f be real-valued FinSequence; ::_thesis: ( |.f.| <> 0 implies ex i being Nat st
( i in dom f & f . i <> 0 ) )
assume  |.f.| <> 0 ; ::_thesis: ex i being Nat st
( i in dom f & f . i <> 0 )
then consider i being Element of NAT  such that
A1: i in dom (sqr f) and
A2: (sqr f) . i <> 0 by PRVECT_2:3, SQUARE_1:17;
take  i ; ::_thesis: ( i in dom f & f . i <> 0 )
thus  i in dom f by A1, VALUED_1:11; ::_thesis: f . i <> 0
 (sqr f) . i = (f . i) ^2 by VALUED_1:11;
hence  f . i <> 0 by A2; ::_thesis: verum
end;

theorem Th21: :: TOPREALC:21
for f being real-valued FinSequence holds abs (Sum f) <= Sum (abs f)
proof
let f be real-valued FinSequence; ::_thesis: abs (Sum f) <= Sum (abs f)
defpred S1[ set ] means  ex F being real-valued FinSequence st
( F = $1 & abs (Sum F) <= Sum (abs F) );
A1: S1[ <*> REAL]
proof
take  <*> REAL ; ::_thesis: ( <*> REAL = <*> REAL & abs (Sum (<*> REAL)) <= Sum (abs (<*> REAL)) )
thus  ( <*> REAL = <*> REAL & abs (Sum (<*> REAL)) <= Sum (abs (<*> REAL)) ) by ABSVALUE:2, RVSUM_1:72; ::_thesis: verum
end;
A2: for p being FinSequence of REAL
for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
given F being real-valued FinSequence such that A3: F = p and
A4: abs (Sum F) <= Sum (abs F) ; ::_thesis: S1[p ^ <*x*>]
A5: (abs (Sum F)) + (abs x) <= (Sum (abs F)) + (abs x) by A4, XREAL_1:6;
take G = p ^ <*x*>; ::_thesis: ( G = p ^ <*x*> & abs (Sum G) <= Sum (abs G) )
A6: abs <*x*> = <*(abs x)*> by JORDAN2B:19;
A7: Sum <*(abs x)*> = abs x by RVSUM_1:73;
 abs G = (abs p) ^ (abs <*x*>) by TOPREAL7:11;
then A8: Sum (abs G) = (Sum (abs p)) + (abs x) by A6, A7, RVSUM_1:75;
 Sum G = (Sum p) + x by RVSUM_1:74;
then  abs (Sum G) <= (abs (Sum p)) + (abs x) by COMPLEX1:56;
hence  ( G = p ^ <*x*> & abs (Sum G) <= Sum (abs G) ) by A8, A3, A5, XXREAL_0:2; ::_thesis: verum
end;
A9: for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A1, A2);
 f is FinSequence of REAL by RVSUM_1:145;
then  S1[f] by A9;
hence  abs (Sum f) <= Sum (abs f) ; ::_thesis: verum
end;

Lm1:  for n being Nat
for f being real-valued b1 -element FinSequence holds f is Element of n -tuples_on REAL
proof
let n be Nat; ::_thesis: for f being real-valued n -element FinSequence holds f is Element of n -tuples_on REAL
let f be real-valued n -element FinSequence; ::_thesis: f is Element of n -tuples_on REAL
A1: f is FinSequence of REAL by RVSUM_1:145;
 len f = n by CARD_1:def_7;
hence  f is Element of n -tuples_on REAL by A1, FINSEQ_2:92; ::_thesis: verum
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
let A be non empty 1-sorted ; ::_thesis: for B being 1 -element 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t
let B be 1 -element 1-sorted ; ::_thesis: for t being Point of B
for f being Function of A,B holds f = A --> t
let t be Point of B; ::_thesis: for f being Function of A,B holds f = A --> t
let f be Function of A,B; ::_thesis: f = A --> t
let a be Element of A; :: according to FUNCT_2:def_8 ::_thesis: f . a = (A --> t) . a
thus  f . a = (A --> t) . a by STRUCT_0:def_10; ::_thesis: verum
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
 ((Seg n) --> T) . i = T by FUNCOP_1:7;
hence  proj (((Seg n) --> T),i) is real-valued ; ::_thesis: verum
end;
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
proof
A1: p (/) r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def_7;
Seg (len (p (/) r)) = dom (p (/) r) by FINSEQ_1:def_3
.= dom p by VALUED_1:def_5
.= Seg n by A2, FINSEQ_1:def_3 ;
then  len (p (/) r) = n by FINSEQ_1:6;
hence  p (/) r is Element of REAL n by A1, FINSEQ_2:92; ::_thesis: verum
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
let m be Nat; ::_thesis: 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) )
let r be real number ; ::_thesis: for p, q being Point of (TOP-REAL m) holds
( p in Ball (q,r) iff - p in Ball ((- q),r) )
let p, q be Point of (TOP-REAL m); ::_thesis: ( p in Ball (q,r) iff - p in Ball ((- q),r) )
A1: m in NAT by ORDINAL1:def_12;
A2: now__::_thesis:_for_a,_b_being_Point_of_(TOP-REAL_m)_st_a_in_Ball_(b,r)_holds_
-_a_in_Ball_((-_b),r)
let a, b be Point of (TOP-REAL m); ::_thesis: ( a in Ball (b,r) implies - a in Ball ((- b),r) )
assume  a in Ball (b,r) ; ::_thesis: - a in Ball ((- b),r)
then A3: |.(a - b).| < r by A1, TOPREAL9:7;
(- a) - (- b) = (- a) + (- (- b))
.= - (a - b) by RLVECT_1:31 ;
then  |.((- a) - (- b)).| = |.(a - b).| by EUCLID:71;
hence  - a in Ball ((- b),r) by A1, A3, TOPREAL9:7; ::_thesis: verum
end;
 ( - (- p) = p & - (- q) = q ) ;
hence  ( p in Ball (q,r) iff - p in Ball ((- q),r) ) by A2; ::_thesis: verum
end;

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
proof
let x be set ; :: according to VALUED_2:def_4,TOPREALC:def_2 ::_thesis: ( not x in the carrier of (TOP-REAL n) or x is set )
assume  x in the carrier of (TOP-REAL n) ; ::_thesis: x is set
then reconsider x = x as Point of (TOP-REAL n) ;
 x is real-valued ;
hence  x is set ; ::_thesis: verum
end;
end;

registration
cluster TOP-REAL 0 ->  real-membered ;
coherence
 TOP-REAL 0 is real-membered
proof
thus  the carrier of (TOP-REAL 0) is real-membered by EUCLID:22, EUCLID:77; :: according to TOPMETR:def_8 ::_thesis: verum
end;
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
proof
let S be 1-sorted ; ::_thesis: ( S is real-functions-membered implies S is complex-functions-membered )
assume A1: the carrier of S is real-functions-membered ; :: according to TOPREALC:def_2 ::_thesis: S is complex-functions-membered
let x be set ; :: according to VALUED_2:def_2,TOPREALC:def_1 ::_thesis: ( not x in the carrier of S or x is set )
thus  ( not x in the carrier of S or x is set ) by A1; ::_thesis: verum
end;
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
take S = 1-sorted(# { the real-valued Function} #); ::_thesis: ( S is strict & not S is empty & S is real-functions-membered )
thus  S is strict ; ::_thesis: ( not S is empty & S is real-functions-membered )
thus  not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is real-functions-membered
let x be set ; :: according to VALUED_2:def_4,TOPREALC:def_2 ::_thesis: ( not x in the carrier of S or x is set )
thus  ( not x in the carrier of S or x is set ) ; ::_thesis: verum
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
take  TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) ; ::_thesis: ( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is strict & not TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is empty & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is real-functions-membered )
thus  ( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is strict & not TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is empty & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is real-functions-membered ) by Def2; ::_thesis: verum
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
let A be SubSpace of S; ::_thesis: A is complex-functions-membered
let x be set ; :: according to VALUED_2:def_2,TOPREALC:def_1 ::_thesis: ( not x in the carrier of A or x is set )
 the carrier of A c= the carrier of S by BORSUK_1:1;
hence  ( not x in the carrier of A or x is set ) ; ::_thesis: verum
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
let A be SubSpace of S; ::_thesis: A is real-functions-membered
let x be set ; :: according to VALUED_2:def_4,TOPREALC:def_2 ::_thesis: ( not x in the carrier of A or x is set )
 the carrier of A c= the carrier of S by BORSUK_1:1;
hence  ( not x in the carrier of A or x is set ) ; ::_thesis: verum
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
set F =  {  (- f) where f is Element of X : f in X  }  ;
  {  (- f) where f is Element of X : f in X  }  is complex-functions-membered
proof
let x be set ; :: according to VALUED_2:def_2 ::_thesis: ( not x in  {  (- f) where f is Element of X : f in X  }  or x is set )
assume  x in  {  (- f) where f is Element of X : f in X  }  ; ::_thesis: x is set
then  ex f being Element of X st
( x = - f & f in X ) ;
hence  x is set ; ::_thesis: verum
end;
then reconsider F =  {  (- f) where f is Element of X : f in X  }  as complex-functions-membered set ;
take  F ; ::_thesis: for f being complex-valued Function holds
( - f in F iff f in X )
let f be complex-valued Function; ::_thesis: ( - f in F iff f in X )
hereby  ::_thesis: ( f in X implies - f in F )
assume  - f in F ; ::_thesis: f in X
then  ex g being Element of X st
( - f = - g & g in X ) ;
hence  f in X by RVSUM_1:24; ::_thesis: verum
end;
thus  ( f in X implies - f in F ) ; ::_thesis: verum
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
let A, B be complex-functions-membered set ; ::_thesis: ( ( for f being complex-valued Function holds
( - f in A iff f in X ) ) & ( for f being complex-valued Function holds
( - f in B iff f in X ) ) implies A = B )
assume that
A1: for f being complex-valued Function holds
( - f in A iff f in X ) and
A2: for f being complex-valued Function holds
( - f in B iff f in X ) ; ::_thesis: A = B
thus  A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A3: x in A ; ::_thesis: x in B
then reconsider x = x as Element of A ;
A4: - (- x) = x ;
then  - x in X by A1, A3;
hence  x in B by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A5: x in B ; ::_thesis: x in A
then reconsider x = x as Element of B ;
A6: - (- x) = x ;
then  - x in X by A2, A5;
hence  x in A by A1, A6; ::_thesis: verum
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
let r, A be complex-functions-membered set ; ::_thesis: ( ( for f being complex-valued Function holds
( - f in r iff f in A ) ) implies for f being complex-valued Function holds
( - f in A iff f in r ) )
assume A7: for f being complex-valued Function holds
( - f in r iff f in A ) ; ::_thesis: for f being complex-valued Function holds
( - f in A iff f in r )
let f be complex-valued Function; ::_thesis: ( - f in A iff f in r )
hereby  ::_thesis: ( f in r implies - f in A )
assume  - f in A ; ::_thesis: f in r
then  - (- f) in r by A7;
hence  f in r ; ::_thesis: verum
end;
assume  f in r ; ::_thesis: - f in A
then  - (- f) in r ;
hence  - f in A by A7; ::_thesis: verum
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
assume  not (-) X is empty ; ::_thesis: contradiction
then consider x being set  such that
A1: x in (-) X by XBOOLE_0:def_1;
reconsider x = x as Element of (-) X by A1;
 - (- x) = x ;
hence  contradiction by A1, Def3; ::_thesis: verum
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
consider x being set  such that
A1: x in X by XBOOLE_0:def_1;
reconsider x = x as Element of X by A1;
 - x in (-) X by Def3;
hence  not (-) X is empty ; ::_thesis: verum
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
let X be complex-functions-membered set ; ::_thesis: for f being complex-valued Function holds
( - f in X iff f in (-) X )
let f be complex-valued Function; ::_thesis: ( - f in X iff f in (-) X )
 ( - (- f) = f & (-) ((-) X) = X ) ;
hence  ( - f in X iff f in (-) X ) by Def3; ::_thesis: verum
end;

registration
let X be real-functions-membered set ;
cluster (-) X ->  complex-functions-membered real-functions-membered ;
coherence
 (-) X is real-functions-membered
proof
let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in (-) X or x is set )
assume A1: x in (-) X ; ::_thesis: x is set
then reconsider x = x as Element of (-) X ;
A2: - x in X by A1, Th24;
 ( - (- x) = x & (-) ((-) X) = X ) ;
hence  x is set by A2; ::_thesis: verum
end;
end;

theorem Th25: :: TOPREALC:25
for n being Nat
for X being Subset of (TOP-REAL n) holds - X = (-) X
proof
let n be Nat; ::_thesis: for X being Subset of (TOP-REAL n) holds - X = (-) X
set T = TOP-REAL n;
let X be Subset of (TOP-REAL n); ::_thesis: - X = (-) X
 for f being complex-valued Function holds
( - f in - X iff f in X )
proof
let f be complex-valued Function; ::_thesis: ( - f in - X iff f in X )
hereby  ::_thesis: ( f in X implies - f in - X )
assume  - f in - X ; ::_thesis: f in X
then consider v being Element of (TOP-REAL n) such that
A1: - f = (- 1) * v and
A2: v in X ;
reconsider g = - f as Element of (TOP-REAL n) by A1;
- g = - (- v) by A1
.= v ;
hence  f in X by A2; ::_thesis: verum
end;
assume A3: f in X ; ::_thesis: - f in - X
then reconsider g = f as Element of (TOP-REAL n) ;
 - g = (- 1) * g ;
hence  - f in - X by A3; ::_thesis: verum
end;
hence  - X = (-) X by Def3; ::_thesis: verum
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
 - X = (-) X by Th25;
hence  (-) X is Subset of (TOP-REAL n) ; ::_thesis: verum
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
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider Y = (-) X as Subset of (TOP-REAL n) ;
 for p being Point of (TOP-REAL n) st p in Y holds
ex r being positive real number st Ball (p,r) c= Y
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p in Y implies ex r being positive real number st Ball (p,r) c= Y )
assume  p in Y ; ::_thesis: ex r being positive real number st Ball (p,r) c= Y
then  - p in (-) Y by Def3;
then consider r being positive real number  such that
A1: Ball ((- p),r) c= X by TOPS_4:2;
take  r ; ::_thesis: Ball (p,r) c= Y
let x be Element of (TOP-REAL n); :: according to LATTICE7:def_1 ::_thesis: ( not x in Ball (p,r) or x in Y )
assume  x in Ball (p,r) ; ::_thesis: x in Y
then  - x in Ball ((- p),r) by Th23;
hence  x in Y by A1, Th24; ::_thesis: verum
end;
hence  for b1 being Subset of (TOP-REAL n) st b1 = (-) X holds
b1 is open by TOPS_4:2; ::_thesis: verum
end;
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
proof
consider x1 being Point of R, x2 being Point of S such that
A1: x = [x1,x2] by BORSUK_1:10;
 f . [x1,x2] is Point of T ;
hence  f . x is Point of T by A1; ::_thesis: verum
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 funcf . (r,s) ->  Point of T;
coherence
 f . (r,s) is Point of T
proof
 f . (r,s) = f . [r,s] ;
hence  f . (r,s) is Point of T ; ::_thesis: verum
end;
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)
proof
A1: p + r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def_7;
Seg (len (p + r)) = dom (p + r) by FINSEQ_1:def_3
.= dom p by VALUED_1:def_2
.= Seg n by A2, FINSEQ_1:def_3 ;
then  len (p + r) = n by FINSEQ_1:6;
then  p + r is Element of REAL n by A1, FINSEQ_2:92;
hence  r + p is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
end;
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)
proof
 p + (- r) is Point of (TOP-REAL n) ;
hence  p - r is Point of (TOP-REAL n) ; ::_thesis: verum
end;
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)
proof
A1: p (#) r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def_7;
Seg (len (p (#) r)) = dom (p (#) r) by FINSEQ_1:def_3
.= dom p by VALUED_1:def_5
.= Seg n by A2, FINSEQ_1:def_3 ;
then  len (p (#) r) = n by FINSEQ_1:6;
then  p (#) r is Element of REAL n by A1, FINSEQ_2:92;
hence  r (#) p is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
end;
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)
proof
reconsider f = p as Element of REAL n by EUCLID:22;
 f (/) r is Element of REAL n ;
hence  p (/) r is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
end;
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)
proof
A1: p1 (#) p2 is FinSequence of REAL by RVSUM_1:145;
A2: ( len p1 = n & len p2 = n ) by CARD_1:def_7;
Seg (len (p1 (#) p2)) = dom (p1 (#) p2) by FINSEQ_1:def_3
.= (dom p1) /\ (dom p2) by VALUED_1:def_4
.= (Seg n) /\ (dom p2) by A2, FINSEQ_1:def_3
.= (Seg n) /\ (Seg n) by A2, FINSEQ_1:def_3 ;
then  len (p1 (#) p2) = n by FINSEQ_1:6;
then  p1 (#) p2 is Element of REAL n by A1, FINSEQ_2:92;
hence  p1 (#) p2 is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
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
 sqr p = p (#) p ;
hence  p ^2 is Point of (TOP-REAL n) ; ::_thesis: verum
end;
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)
proof
A1: p1 /" p2 is FinSequence of REAL by RVSUM_1:145;
A2: ( len p1 = n & len p2 = n ) by CARD_1:def_7;
Seg (len (p1 /" p2)) = dom (p1 /" p2) by FINSEQ_1:def_3
.= (dom p1) /\ (dom p2) by VALUED_1:16
.= (Seg n) /\ (dom p2) by A2, FINSEQ_1:def_3
.= (Seg n) /\ (Seg n) by A2, FINSEQ_1:def_3 ;
then  len (p1 /" p2) = n by FINSEQ_1:6;
then  p1 /" p2 is Element of REAL n by A1, FINSEQ_2:92;
hence  p1 /" p2 is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
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 funcp +* (x,r) ->  Point of (TOP-REAL n);
coherence
 p +* (x,r) is Point of (TOP-REAL n)
proof
A1: p +* (x,r) is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def_7;
Seg (len (p +* (x,r))) = dom (p +* (x,r)) by FINSEQ_1:def_3
.= dom p by FUNCT_7:30
.= Seg n by A2, FINSEQ_1:def_3 ;
then  len (p +* (x,r)) = n by FINSEQ_1:6;
then  p +* (x,r) is Element of REAL n by A1, FINSEQ_2:92;
hence  p +* (x,r) is Point of (TOP-REAL n) by EUCLID:22; ::_thesis: verum
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
let n be Nat; ::_thesis: 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
let r be real number ; ::_thesis: for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball (o,r) holds
abs (Sum (a - o)) < n * r
let a, o be Point of (TOP-REAL n); ::_thesis: ( n <> 0 & a in Ball (o,r) implies abs (Sum (a - o)) < n * r )
set R1 = a - o;
set R2 = n |-> r;
assume that
A1: n <> 0 and
A2: a in Ball (o,r) ; ::_thesis: abs (Sum (a - o)) < n * r
A3: Sum (n |-> r) = n * r by RVSUM_1:80;
A4: ( abs (a - o) is Element of n -tuples_on REAL & n |-> r is Element of n -tuples_on REAL ) by Lm1;
A5: for j being Nat st j in Seg n holds
(abs (a - o)) . j < (n |-> r) . j
proof
let j be Nat; ::_thesis: ( j in Seg n implies (abs (a - o)) . j < (n |-> r) . j )
assume  j in Seg n ; ::_thesis: (abs (a - o)) . j < (n |-> r) . j
then A6: (n |-> r) . j = r by FINSEQ_2:57;
 abs ((a - o) . j) < r by A2, EUCLID_9:9;
hence  (abs (a - o)) . j < (n |-> r) . j by A6, VALUED_1:18; ::_thesis: verum
end;
then A7: for j being Nat st j in Seg n holds
(abs (a - o)) . j <= (n |-> r) . j ;
 ex j being Nat st
( j in Seg n & (abs (a - o)) . j < (n |-> r) . j )
proof
take  1 ; ::_thesis: ( 1 in Seg n & (abs (a - o)) . 1 < (n |-> r) . 1 )
 1 <= n by A1, NAT_1:14;
hence  1 in Seg n ; ::_thesis: (abs (a - o)) . 1 < (n |-> r) . 1
hence  (abs (a - o)) . 1 < (n |-> r) . 1 by A5; ::_thesis: verum
end;
then A8: Sum (abs (a - o)) < Sum (n |-> r) by A7, A4, RVSUM_1:83;
 abs (Sum (a - o)) <= Sum (abs (a - o)) by Th21;
hence  abs (Sum (a - o)) < n * r by A3, A8, XXREAL_0:2; ::_thesis: verum
end;

registration
let n be Nat;
cluster Euclid n ->  real-functions-membered ;
coherence
 Euclid n is real-functions-membered
proof
let x be set ; :: according to VALUED_2:def_4,TOPREALC:def_2 ::_thesis: ( not x in the carrier of (Euclid n) or x is set )
assume  x in the carrier of (Euclid n) ; ::_thesis: x is set
then reconsider x = x as Point of (Euclid n) ;
 x is real-valued ;
hence  x is set ; ::_thesis: verum
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
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V holds (v + u) - u = v
let v, u be Element of V; ::_thesis: (v + u) - u = v
thus (v + u) - u = v + (u - u) by RLVECT_1:28
.= v + (0. V) by RLVECT_1:5
.= v by RLVECT_1:4 ; ::_thesis: verum
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
let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v, u being Element of V holds (v - u) + u = v
let v, u be Element of V; ::_thesis: (v - u) + u = v
thus (v - u) + u = v - (u - u) by RLVECT_1:29
.= v - (0. V) by RLVECT_1:5
.= v by RLVECT_1:13 ; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let c be complex number ; ::_thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [+] c = f <+> ((dom f) --> c)
let Y be complex-functions-membered set ; ::_thesis: for f being PartFunc of X,Y holds f [+] c = f <+> ((dom f) --> c)
let f be PartFunc of X,Y; ::_thesis: f [+] c = f <+> ((dom f) --> c)
set g = (dom f) --> c;
A1: dom (f [+] c) = dom f by VALUED_2:def_37;
A2: dom (f <+> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:def_41;
A3: dom ((dom f) --> c) = dom f by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_[+]_c)_holds_
(f_[+]_c)_._x_=_(f_<+>_((dom_f)_-->_c))_._x
let x be set ; ::_thesis: ( x in dom (f [+] c) implies (f [+] c) . x = (f <+> ((dom f) --> c)) . x )
assume A4: x in dom (f [+] c) ; ::_thesis: (f [+] c) . x = (f <+> ((dom f) --> c)) . x
hence (f [+] c) . x = (f . x) + c by VALUED_2:def_37
.= (f . x) + (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7
.= (f <+> ((dom f) --> c)) . x by A1, A2, A3, A4, VALUED_2:def_41 ;
::_thesis: verum
end;
hence  f [+] c = f <+> ((dom f) --> c) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let c be complex number ; ::_thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [-] c = f <-> ((dom f) --> c)
let Y be complex-functions-membered set ; ::_thesis: for f being PartFunc of X,Y holds f [-] c = f <-> ((dom f) --> c)
let f be PartFunc of X,Y; ::_thesis: f [-] c = f <-> ((dom f) --> c)
set g = (dom f) --> c;
A1: dom (f [-] c) = dom f by VALUED_2:def_37;
A2: dom (f <-> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:61;
A3: dom ((dom f) --> c) = dom f by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_[-]_c)_holds_
(f_[-]_c)_._x_=_(f_<->_((dom_f)_-->_c))_._x
let x be set ; ::_thesis: ( x in dom (f [-] c) implies (f [-] c) . x = (f <-> ((dom f) --> c)) . x )
assume A4: x in dom (f [-] c) ; ::_thesis: (f [-] c) . x = (f <-> ((dom f) --> c)) . x
hence (f [-] c) . x = (f . x) - c by VALUED_2:def_37
.= (f . x) - (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7
.= (f <-> ((dom f) --> c)) . x by A1, A2, A3, A4, VALUED_2:62 ;
::_thesis: verum
end;
hence  f [-] c = f <-> ((dom f) --> c) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let c be complex number ; ::_thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
let Y be complex-functions-membered set ; ::_thesis: for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
let f be PartFunc of X,Y; ::_thesis: f [#] c = f <#> ((dom f) --> c)
set g = (dom f) --> c;
A1: dom (f [#] c) = dom f by VALUED_2:def_39;
A2: dom (f <#> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:def_43;
A3: dom ((dom f) --> c) = dom f by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_[#]_c)_holds_
(f_[#]_c)_._x_=_(f_<#>_((dom_f)_-->_c))_._x
let x be set ; ::_thesis: ( x in dom (f [#] c) implies (f [#] c) . x = (f <#> ((dom f) --> c)) . x )
assume A4: x in dom (f [#] c) ; ::_thesis: (f [#] c) . x = (f <#> ((dom f) --> c)) . x
hence (f [#] c) . x = c (#) (f . x) by VALUED_2:def_39
.= (f . x) (#) (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7
.= (f <#> ((dom f) --> c)) . x by A1, A2, A3, A4, VALUED_2:def_43 ;
::_thesis: verum
end;
hence  f [#] c = f <#> ((dom f) --> c) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let c be complex number ; ::_thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [/] c = f </> ((dom f) --> c)
let Y be complex-functions-membered set ; ::_thesis: for f being PartFunc of X,Y holds f [/] c = f </> ((dom f) --> c)
let f be PartFunc of X,Y; ::_thesis: f [/] c = f </> ((dom f) --> c)
set g = (dom f) --> c;
A1: dom (f [/] c) = dom f by VALUED_2:def_39;
A2: dom (f </> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:71;
A3: dom ((dom f) --> c) = dom f by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_[/]_c)_holds_
(f_[/]_c)_._x_=_(f_</>_((dom_f)_-->_c))_._x
let x be set ; ::_thesis: ( x in dom (f [/] c) implies (f [/] c) . x = (f </> ((dom f) --> c)) . x )
assume A4: x in dom (f [/] c) ; ::_thesis: (f [/] c) . x = (f </> ((dom f) --> c)) . x
hence (f [/] c) . x = (f . x) (/) c by VALUED_2:56
.= (f . x) (/) (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7
.= (f </> ((dom f) --> c)) . x by A1, A2, A3, A4, VALUED_2:72 ;
::_thesis: verum
end;
hence  f [/] c = f </> ((dom f) --> c) by A1, A2, A3, FUNCT_1:2; ::_thesis: verum
end;

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
proof
 dom (f <++> g) = (dom f) /\ (dom g) by VALUED_2:def_45;
hence  f <++> g is FinSequence-like by VALUED_1:19; ::_thesis: verum
end;
clusterf <--> g ->  FinSequence-like ;
coherence
 f <--> g is FinSequence-like
proof
 dom (f <--> g) = (dom f) /\ (dom g) by VALUED_2:def_46;
hence  f <--> g is FinSequence-like by VALUED_1:19; ::_thesis: verum
end;
clusterf <##> g ->  FinSequence-like ;
coherence
 f <##> g is FinSequence-like
proof
 dom (f <##> g) = (dom f) /\ (dom g) by VALUED_2:def_47;
hence  f <##> g is FinSequence-like by VALUED_1:19; ::_thesis: verum
end;
clusterf <//> g ->  FinSequence-like ;
coherence
 f <//> g is FinSequence-like
proof
 dom (f <//> g) = (dom f) /\ (dom g) by VALUED_2:def_48;
hence  f <//> g is FinSequence-like by VALUED_1:19; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Nat
for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)
let n be Nat; ::_thesis: for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)
let f be Function of X,(TOP-REAL n); ::_thesis: <-> f is Function of X,(TOP-REAL n)
set g = <-> f;
A1: dom (<-> f) = dom f by VALUED_2:def_33;
A2: dom f = X by FUNCT_2:def_1;
 for x being set st x in X holds
(<-> f) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (<-> f) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (<-> f) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
A4: - (f . x) = - (f . x) ;
 (<-> f) . x = - (f . x) by A1, A2, VALUED_2:def_33;
hence  (<-> f) . x in the carrier of (TOP-REAL n) by A4; ::_thesis: verum
end;
hence  <-> f is Function of X,(TOP-REAL n) by A1, A2, FUNCT_2:3; ::_thesis: verum
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
let i, n be Nat; ::_thesis: for f being Function of (TOP-REAL i),(TOP-REAL n) holds f (-) is Function of (TOP-REAL i),(TOP-REAL n)
set X = the carrier of (TOP-REAL i);
let f be Function of the carrier of (TOP-REAL i),(TOP-REAL n); ::_thesis: f (-) is Function of (TOP-REAL i),(TOP-REAL n)
set g = f (-) ;
A1: dom (f (-)) = dom f by VALUED_2:def_34;
A2: dom f = the carrier of (TOP-REAL i) by FUNCT_2:def_1;
 for x being set st x in the carrier of (TOP-REAL i) holds
(f (-)) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL i) implies (f (-)) . x in the carrier of (TOP-REAL n) )
assume  x in the carrier of (TOP-REAL i) ; ::_thesis: (f (-)) . x in the carrier of (TOP-REAL n)
then reconsider x = x as Element of the carrier of (TOP-REAL i) ;
reconsider y = - x as Element of the carrier of (TOP-REAL i) ;
reconsider f = f as Function of the carrier of (TOP-REAL i),(TOP-REAL n) ;
 (f (-)) . x = f . y by A1, A2, VALUED_2:def_34;
hence  (f (-)) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f (-) is Function of (TOP-REAL i),(TOP-REAL n) by A1, A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: for r being real number
for f being Function of X,(TOP-REAL n) holds f [+] r is Function of X,(TOP-REAL n)
let r be real number ; ::_thesis: for f being Function of X,(TOP-REAL n) holds f [+] r is Function of X,(TOP-REAL n)
let f be Function of X,(TOP-REAL n); ::_thesis: f [+] r is Function of X,(TOP-REAL n)
set h = f [+] r;
 dom f = X by FUNCT_2:def_1;
then A1: dom (f [+] r) = X by VALUED_2:def_37;
 for x being set st x in X holds
(f [+] r) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f [+] r) . x in the carrier of (TOP-REAL n) )
assume A2: x in X ; ::_thesis: (f [+] r) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A2;
reconsider f = f as Function of X,(TOP-REAL n) ;
A3: (f . x) + r = (f . x) + r ;
 (f [+] r) . x = (f . x) + r by A1, VALUED_2:def_37;
hence  (f [+] r) . x in the carrier of (TOP-REAL n) by A3; ::_thesis: verum
end;
hence  f [+] r is Function of X,(TOP-REAL n) by A1, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: for r being real number
for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)
let r be real number ; ::_thesis: for f being Function of X,(TOP-REAL n) holds f [#] r is Function of X,(TOP-REAL n)
let f be Function of X,(TOP-REAL n); ::_thesis: f [#] r is Function of X,(TOP-REAL n)
set h = f [#] r;
 dom f = X by FUNCT_2:def_1;
then A1: dom (f [#] r) = X by VALUED_2:def_39;
 for x being set st x in X holds
(f [#] r) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f [#] r) . x in the carrier of (TOP-REAL n) )
assume A2: x in X ; ::_thesis: (f [#] r) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A2;
reconsider f = f as Function of X,(TOP-REAL n) ;
A3: (f . x) (#) r = (f . x) (#) r ;
 (f [#] r) . x = (f . x) (#) r by A1, VALUED_2:def_39;
hence  (f [#] r) . x in the carrier of (TOP-REAL n) by A3; ::_thesis: verum
end;
hence  f [#] r is Function of X,(TOP-REAL n) by A1, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)
let n be Nat; ::_thesis: for f, g being Function of X,(TOP-REAL n) holds f <++> g is Function of X,(TOP-REAL n)
let f, g be Function of X,(TOP-REAL n); ::_thesis: f <++> g is Function of X,(TOP-REAL n)
set h = f <++> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <++> g) = X by A1, VALUED_2:def_45;
 for x being set st x in X holds
(f <++> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <++> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <++> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f, g = g as Function of X,(TOP-REAL n) ;
A4: (f . x) + (g . x) = (f . x) + (g . x) ;
 (f <++> g) . x = (f . x) + (g . x) by A2, VALUED_2:def_45;
hence  (f <++> g) . x in the carrier of (TOP-REAL n) by A4; ::_thesis: verum
end;
hence  f <++> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <--> g is Function of X,(TOP-REAL n)
let n be Nat; ::_thesis: for f, g being Function of X,(TOP-REAL n) holds f <--> g is Function of X,(TOP-REAL n)
let f, g be Function of X,(TOP-REAL n); ::_thesis: f <--> g is Function of X,(TOP-REAL n)
set h = f <--> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <--> g) = X by A1, VALUED_2:def_46;
 for x being set st x in X holds
(f <--> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <--> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <--> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f, g = g as Function of X,(TOP-REAL n) ;
A4: (f . x) - (g . x) = (f . x) - (g . x) ;
 (f <--> g) . x = (f . x) - (g . x) by A2, VALUED_2:def_46;
hence  (f <--> g) . x in the carrier of (TOP-REAL n) by A4; ::_thesis: verum
end;
hence  f <--> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <##> g is Function of X,(TOP-REAL n)
let n be Nat; ::_thesis: for f, g being Function of X,(TOP-REAL n) holds f <##> g is Function of X,(TOP-REAL n)
let f, g be Function of X,(TOP-REAL n); ::_thesis: f <##> g is Function of X,(TOP-REAL n)
set h = f <##> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <##> g) = X by A1, VALUED_2:def_47;
 for x being set st x in X holds
(f <##> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <##> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <##> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f, g = g as Function of X,(TOP-REAL n) ;
 (f <##> g) . x = (f . x) (#) (g . x) by A2, VALUED_2:def_47;
hence  (f <##> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f <##> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Nat
for f, g being Function of X,(TOP-REAL n) holds f <//> g is Function of X,(TOP-REAL n)
let n be Nat; ::_thesis: for f, g being Function of X,(TOP-REAL n) holds f <//> g is Function of X,(TOP-REAL n)
let f, g be Function of X,(TOP-REAL n); ::_thesis: f <//> g is Function of X,(TOP-REAL n)
set h = f <//> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <//> g) = X by A1, VALUED_2:def_48;
 for x being set st x in X holds
(f <//> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <//> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <//> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f, g = g as Function of X,(TOP-REAL n) ;
 (f <//> g) . x = (f . x) /" (g . x) by A2, VALUED_2:def_48;
hence  (f <//> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f <//> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: 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)
let f be Function of X,(TOP-REAL n); ::_thesis: for g being Function of X,R^1 holds f <+> g is Function of X,(TOP-REAL n)
let g be Function of X,R^1; ::_thesis: f <+> g is Function of X,(TOP-REAL n)
set h = f <+> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <+> g) = X by A1, VALUED_2:def_41;
 for x being set st x in X holds
(f <+> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <+> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <+> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
 (f <+> g) . x = (f . x) + (g . x) by A2, VALUED_2:def_41;
hence  (f <+> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f <+> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: 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)
let f be Function of X,(TOP-REAL n); ::_thesis: for g being Function of X,R^1 holds f <-> g is Function of X,(TOP-REAL n)
let g be Function of X,R^1; ::_thesis: f <-> g is Function of X,(TOP-REAL n)
set h = f <-> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <-> g) = X by A1, VALUED_2:61;
 for x being set st x in X holds
(f <-> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <-> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <-> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
 (f <-> g) . x = (f . x) - (g . x) by A2, VALUED_2:62;
hence  (f <-> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f <-> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: 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)
let f be Function of X,(TOP-REAL n); ::_thesis: for g being Function of X,R^1 holds f <#> g is Function of X,(TOP-REAL n)
let g be Function of X,R^1; ::_thesis: f <#> g is Function of X,(TOP-REAL n)
set h = f <#> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f <#> g) = X by A1, VALUED_2:def_43;
 for x being set st x in X holds
(f <#> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f <#> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f <#> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
 (f <#> g) . x = (f . x) (#) (g . x) by A2, VALUED_2:def_43;
hence  (f <#> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f <#> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let n be Nat; ::_thesis: 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)
let f be Function of X,(TOP-REAL n); ::_thesis: for g being Function of X,R^1 holds f </> g is Function of X,(TOP-REAL n)
let g be Function of X,R^1; ::_thesis: f </> g is Function of X,(TOP-REAL n)
set h = f </> g;
A1: dom f = X by FUNCT_2:def_1;
 dom g = X by FUNCT_2:def_1;
then A2: dom (f </> g) = X by A1, VALUED_2:71;
 for x being set st x in X holds
(f </> g) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in X implies (f </> g) . x in the carrier of (TOP-REAL n) )
assume A3: x in X ; ::_thesis: (f </> g) . x in the carrier of (TOP-REAL n)
then reconsider X = X as non empty set ;
reconsider x = x as Element of X by A3;
reconsider f = f as Function of X,(TOP-REAL n) ;
 (f </> g) . x = (f . x) (/) (g . x) by A2, VALUED_2:72;
hence  (f </> g) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f </> g is Function of X,(TOP-REAL n) by A2, FUNCT_2:3; ::_thesis: verum
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
defpred S1[ set , set ] means $2 = n |-> (f . $1);
A1: for x being Element of T ex y being Element of (TOP-REAL n) st S1[x,y]
proof
let x be Element of T; ::_thesis: ex y being Element of (TOP-REAL n) st S1[x,y]
 f . x in REAL by XREAL_0:def_1;
then  n |-> (f . x) is Element of REAL n by FINSEQ_2:112;
then reconsider y = n |-> (f . x) as Point of (TOP-REAL n) by EUCLID:22;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
 ex F being Function of T,(TOP-REAL n) st
for x being Element of T holds S1[x,F . x] from FUNCT_2:sch_3(A1);
hence  ex b1 being Function of T,(TOP-REAL n) st
for t being Element of T holds b1 . t = n |-> (f . t) ; ::_thesis: verum
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
let F, G be Function of T,(TOP-REAL n); ::_thesis: ( ( for t being Element of T holds F . t = n |-> (f . t) ) & ( for t being Element of T holds G . t = n |-> (f . t) ) implies F = G )
assume that
A2: for t being Element of T holds F . t = n |-> (f . t) and
A3: for t being Element of T holds G . t = n |-> (f . t) ; ::_thesis: F = G
let t be Element of T; :: according to FUNCT_2:def_8 ::_thesis: F . t = G . t
thus F . t = n |-> (f . t) by A2
.= G . t by A3 ; ::_thesis: verum
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
let x be set ; ::_thesis: 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
let n be Nat; ::_thesis: 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
let T be non empty TopSpace; ::_thesis: 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
let R be real-membered set ; ::_thesis: 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
let f be Function of T,R; ::_thesis: for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let t be Point of T; ::_thesis: ( x in Seg n implies ((incl (f,n)) . t) . x = f . t )
assume A1: x in Seg n ; ::_thesis: ((incl (f,n)) . t) . x = f . t
thus ((incl (f,n)) . t) . x = (n |-> (f . t)) . x by Def4
.= f . t by A1, FINSEQ_2:57 ; ::_thesis: verum
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
let T be non empty set ; ::_thesis: for R being real-membered set
for f being Function of T,R holds incl (f,0) = T --> 0
let R be real-membered set ; ::_thesis: for f being Function of T,R holds incl (f,0) = T --> 0
let f be Function of T,R; ::_thesis: incl (f,0) = T --> 0
reconsider z = 0 as Element of (TOP-REAL 0) ;
 incl (f,0) = T --> z
proof
let x be Element of T; :: according to FUNCT_2:def_8 ::_thesis: (incl (f,0)) . x = (T --> z) . x
thus  (incl (f,0)) . x = (T --> z) . x ; ::_thesis: verum
end;
hence  incl (f,0) = T --> 0 ; ::_thesis: verum
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
let n be Nat; ::_thesis: 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))
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <+> g = f <++> (incl (g,n))
let f be Function of T,(TOP-REAL n); ::_thesis: for g being Function of T,R^1 holds f <+> g = f <++> (incl (g,n))
let g be Function of T,R^1; ::_thesis: f <+> g = f <++> (incl (g,n))
set I = incl (g,n);
reconsider h = f <+> g as Function of T,(TOP-REAL n) by Th43;
reconsider G = f <++> (incl (g,n)) as Function of T,(TOP-REAL n) by Th39;
 h = G
proof
let t be Point of T; :: according to FUNCT_2:def_8 ::_thesis: h . t = G . t
A1: dom h = the carrier of T by FUNCT_2:def_1;
A2: (f . t) + ((incl (g,n)) . t) = (f . t) + (g . t)
proof
A3: ( dom (f . t) = Seg n & dom ((incl (g,n)) . t) = Seg n ) by FINSEQ_1:89;
A4: dom ((f . t) + ((incl (g,n)) . t)) = (dom (f . t)) /\ (dom ((incl (g,n)) . t)) by VALUED_1:def_1
.= Seg n by A3 ;
A5: dom ((f . t) + (g . t)) = dom (f . t) by VALUED_1:def_2;
thus  dom ((f . t) + ((incl (g,n)) . t)) = dom ((f . t) + (g . t)) by A4, FINSEQ_1:89; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f . t) + ((incl (g,n)) . t)) or ((f . t) + ((incl (g,n)) . t)) . b1 = ((f . t) + (g . t)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f . t) + ((incl (g,n)) . t)) or ((f . t) + ((incl (g,n)) . t)) . x = ((f . t) + (g . t)) . x )
assume A6: x in dom ((f . t) + ((incl (g,n)) . t)) ; ::_thesis: ((f . t) + ((incl (g,n)) . t)) . x = ((f . t) + (g . t)) . x
hence ((f . t) + ((incl (g,n)) . t)) . x = ((f . t) . x) + (((incl (g,n)) . t) . x) by VALUED_1:def_1
.= ((f . t) . x) + (g . t) by A4, A6, Th47
.= ((f . t) + (g . t)) . x by A3, A4, A6, A5, VALUED_1:def_2 ;
::_thesis: verum
end;
 dom G = the carrier of T by FUNCT_2:def_1;
hence G . t = (f . t) + ((incl (g,n)) . t) by VALUED_2:def_45
.= h . t by A1, A2, VALUED_2:def_41 ;
::_thesis: verum
end;
hence  f <+> g = f <++> (incl (g,n)) ; ::_thesis: verum
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
let n be Nat; ::_thesis: 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))
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <-> g = f <--> (incl (g,n))
let f be Function of T,(TOP-REAL n); ::_thesis: for g being Function of T,R^1 holds f <-> g = f <--> (incl (g,n))
let g be Function of T,R^1; ::_thesis: f <-> g = f <--> (incl (g,n))
set I = incl (g,n);
reconsider h = f <-> g as Function of T,(TOP-REAL n) by Th44;
reconsider G = f <--> (incl (g,n)) as Function of T,(TOP-REAL n) by Th40;
 h = G
proof
let t be Point of T; :: according to FUNCT_2:def_8 ::_thesis: h . t = G . t
A1: dom h = the carrier of T by FUNCT_2:def_1;
A2: (f . t) - ((incl (g,n)) . t) = (f . t) - (g . t)
proof
A3: ( dom (f . t) = Seg n & dom ((incl (g,n)) . t) = Seg n ) by FINSEQ_1:89;
A4: dom ((f . t) - ((incl (g,n)) . t)) = (dom (f . t)) /\ (dom ((incl (g,n)) . t)) by VALUED_1:12
.= Seg n by A3 ;
A5: dom ((f . t) - (g . t)) = dom (f . t) by VALUED_1:def_2;
thus  dom ((f . t) - ((incl (g,n)) . t)) = dom ((f . t) - (g . t)) by A4, FINSEQ_1:89; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f . t) - ((incl (g,n)) . t)) or ((f . t) - ((incl (g,n)) . t)) . b1 = ((f . t) - (g . t)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f . t) - ((incl (g,n)) . t)) or ((f . t) - ((incl (g,n)) . t)) . x = ((f . t) - (g . t)) . x )
assume A6: x in dom ((f . t) - ((incl (g,n)) . t)) ; ::_thesis: ((f . t) - ((incl (g,n)) . t)) . x = ((f . t) - (g . t)) . x
hence ((f . t) - ((incl (g,n)) . t)) . x = ((f . t) . x) - (((incl (g,n)) . t) . x) by VALUED_1:13
.= ((f . t) . x) - (g . t) by A4, A6, Th47
.= ((f . t) - (g . t)) . x by A3, A4, A6, A5, VALUED_1:def_2 ;
::_thesis: verum
end;
 dom G = the carrier of T by FUNCT_2:def_1;
hence G . t = (f . t) - ((incl (g,n)) . t) by VALUED_2:def_46
.= h . t by A1, A2, VALUED_2:62 ;
::_thesis: verum
end;
hence  f <-> g = f <--> (incl (g,n)) ; ::_thesis: verum
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
let n be Nat; ::_thesis: 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))
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <#> g = f <##> (incl (g,n))
let f be Function of T,(TOP-REAL n); ::_thesis: for g being Function of T,R^1 holds f <#> g = f <##> (incl (g,n))
let g be Function of T,R^1; ::_thesis: f <#> g = f <##> (incl (g,n))
set I = incl (g,n);
reconsider h = f <#> g as Function of T,(TOP-REAL n) by Th45;
reconsider G = f <##> (incl (g,n)) as Function of T,(TOP-REAL n) by Th41;
 h = G
proof
let t be Point of T; :: according to FUNCT_2:def_8 ::_thesis: h . t = G . t
A1: dom h = the carrier of T by FUNCT_2:def_1;
A2: (f . t) (#) ((incl (g,n)) . t) = (f . t) (#) (g . t)
proof
A3: ( dom (f . t) = Seg n & dom ((incl (g,n)) . t) = Seg n ) by FINSEQ_1:89;
A4: dom ((f . t) (#) ((incl (g,n)) . t)) = (dom (f . t)) /\ (dom ((incl (g,n)) . t)) by VALUED_1:def_4
.= Seg n by A3 ;
hence  dom ((f . t) (#) ((incl (g,n)) . t)) = dom ((f . t) (#) (g . t)) by FINSEQ_1:89; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f . t) (#) ((incl (g,n)) . t)) or ((f . t) (#) ((incl (g,n)) . t)) . b1 = ((f . t) (#) (g . t)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f . t) (#) ((incl (g,n)) . t)) or ((f . t) (#) ((incl (g,n)) . t)) . x = ((f . t) (#) (g . t)) . x )
assume A5: x in dom ((f . t) (#) ((incl (g,n)) . t)) ; ::_thesis: ((f . t) (#) ((incl (g,n)) . t)) . x = ((f . t) (#) (g . t)) . x
hence ((f . t) (#) ((incl (g,n)) . t)) . x = ((f . t) . x) * (((incl (g,n)) . t) . x) by VALUED_1:def_4
.= ((f . t) . x) * (g . t) by A4, A5, Th47
.= ((f . t) (#) (g . t)) . x by VALUED_1:6 ;
::_thesis: verum
end;
 dom G = the carrier of T by FUNCT_2:def_1;
hence G . t = (f . t) (#) ((incl (g,n)) . t) by VALUED_2:def_47
.= h . t by A1, A2, VALUED_2:def_43 ;
::_thesis: verum
end;
hence  f <#> g = f <##> (incl (g,n)) ; ::_thesis: verum
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
let n be Nat; ::_thesis: 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))
let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f </> g = f <//> (incl (g,n))
let f be Function of T,(TOP-REAL n); ::_thesis: for g being Function of T,R^1 holds f </> g = f <//> (incl (g,n))
let g be Function of T,R^1; ::_thesis: f </> g = f <//> (incl (g,n))
set I = incl (g,n);
reconsider h = f </> g as Function of T,(TOP-REAL n) by Th46;
reconsider G = f <//> (incl (g,n)) as Function of T,(TOP-REAL n) by Th42;
 h = G
proof
let t be Point of T; :: according to FUNCT_2:def_8 ::_thesis: h . t = G . t
A1: dom h = the carrier of T by FUNCT_2:def_1;
A2: (f . t) /" ((incl (g,n)) . t) = (f . t) (#) ((g ") . t)
proof
A3: ( dom (f . t) = Seg n & dom ((incl (g,n)) . t) = Seg n ) by FINSEQ_1:89;
A4: dom ((f . t) /" ((incl (g,n)) . t)) = (dom (f . t)) /\ (dom ((incl (g,n)) . t)) by VALUED_1:16
.= Seg n by A3 ;
hence  dom ((f . t) /" ((incl (g,n)) . t)) = dom ((f . t) (#) ((g ") . t)) by FINSEQ_1:89; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom ((f . t) /" ((incl (g,n)) . t)) or ((f . t) /" ((incl (g,n)) . t)) . b1 = ((f . t) (#) ((g ") . t)) . b1 )
let x be set ; ::_thesis: ( not x in dom ((f . t) /" ((incl (g,n)) . t)) or ((f . t) /" ((incl (g,n)) . t)) . x = ((f . t) (#) ((g ") . t)) . x )
assume A5: x in dom ((f . t) /" ((incl (g,n)) . t)) ; ::_thesis: ((f . t) /" ((incl (g,n)) . t)) . x = ((f . t) (#) ((g ") . t)) . x
thus ((f . t) /" ((incl (g,n)) . t)) . x = ((f . t) . x) / (((incl (g,n)) . t) . x) by VALUED_1:17
.= ((f . t) . x) / (g . t) by A4, A5, Th47
.= ((f . t) . x) * ((g ") . t) by VALUED_1:10
.= ((f . t) (#) ((g ") . t)) . x by VALUED_1:6 ; ::_thesis: verum
end;
 dom G = the carrier of T by FUNCT_2:def_1;
hence G . t = (f . t) /" ((incl (g,n)) . t) by VALUED_2:def_48
.= h . t by A1, A2, VALUED_2:def_43 ;
::_thesis: verum
end;
hence  f </> g = f <//> (incl (g,n)) ; ::_thesis: verum
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
deffunc H1( Point of (TOP-REAL n), Point of (TOP-REAL n)) ->  Point of (TOP-REAL n) = $1 (#) $2;
 ex f being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n) st
for x, y being Element of the carrier of (TOP-REAL n) holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
hence  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 by A1; ::_thesis: verum
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
let f, g be Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n); ::_thesis: ( ( for x, y being Point of (TOP-REAL n) holds f . (x,y) = x (#) y ) & ( for x, y being Point of (TOP-REAL n) holds g . (x,y) = x (#) y ) implies f = g )
assume that
A2: for x, y being Point of (TOP-REAL n) holds f . (x,y) = x (#) y and
A3: for x, y being Point of (TOP-REAL n) holds g . (x,y) = x (#) y ; ::_thesis: f = g
now__::_thesis:_for_x,_y_being_Point_of_(TOP-REAL_n)_holds_f_._(x,y)_=_g_._(x,y)
let x, y be Point of (TOP-REAL n); ::_thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = x (#) y by A2
.= g . (x,y) by A3 ; ::_thesis: verum
end;
hence  f = g by A1, BINOP_1:2; ::_thesis: verum
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
set T = TOP-REAL 0;
let x be Element of the carrier of [:(TOP-REAL 0),(TOP-REAL 0):]; :: according to FUNCT_2:def_8 ::_thesis: (TIMES 0) . x = ([:(TOP-REAL 0),(TOP-REAL 0):] --> (0. (TOP-REAL 0))) . x
thus  (TIMES 0) . x = ([:(TOP-REAL 0),(TOP-REAL 0):] --> (0. (TOP-REAL 0))) . x ; ::_thesis: verum
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
let n be Nat; ::_thesis: for T being non empty TopSpace
for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: (f,g)
let T be non empty TopSpace; ::_thesis: for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: (f,g)
set R = TOP-REAL n;
set F = TIMES n;
let f, g be Function of T,(TOP-REAL n); ::_thesis: f <##> g = (TIMES n) .: (f,g)
A1: dom (f <##> g) = (dom f) /\ (dom g) by VALUED_2:def_47;
dom (TIMES n) = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by FUNCT_2:def_1
.= [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2 ;
then  [:(rng f),(rng g):] c= dom (TIMES n) by ZFMISC_1:96;
then A2: dom ((TIMES n) .: (f,g)) = (dom f) /\ (dom g) by FUNCOP_1:69;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_<##>_g)_holds_
(f_<##>_g)_._x_=_((TIMES_n)_.:_(f,g))_._x
let x be set ; ::_thesis: ( x in dom (f <##> g) implies (f <##> g) . x = ((TIMES n) .: (f,g)) . x )
assume A3: x in dom (f <##> g) ; ::_thesis: (f <##> g) . x = ((TIMES n) .: (f,g)) . x
then A4: ( f . x is Point of (TOP-REAL n) & g . x is Point of (TOP-REAL n) ) by FUNCT_2:5;
thus (f <##> g) . x = (f . x) (#) (g . x) by A3, VALUED_2:def_47
.= (TIMES n) . ((f . x),(g . x)) by A4, Def5
.= ((TIMES n) .: (f,g)) . x by A1, A2, A3, FUNCOP_1:22 ; ::_thesis: verum
end;
hence  f <##> g = (TIMES n) .: (f,g) by A1, A2, FUNCT_1:2; ::_thesis: verum
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
let F, G be Function of (TOP-REAL m),R^1; ::_thesis: ( ( for p being Element of (TOP-REAL m) holds F . p = p /. n ) & ( for p being Element of (TOP-REAL m) holds G . p = p /. n ) implies F = G )
assume that
A2: for p being Element of (TOP-REAL m) holds F . p = p /. n and
A3: for p being Element of (TOP-REAL m) holds G . p = p /. n ; ::_thesis: F = G
let p be Element of (TOP-REAL m); :: according to FUNCT_2:def_8 ::_thesis: F . p = G . p
thus F . p = p /. n by A2
.= G . p by A3 ; ::_thesis: verum
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
let m, n be Nat; ::_thesis: 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).[
let r be real number ; ::_thesis: 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).[
let p be Point of (TOP-REAL m); ::_thesis: ( n in dom p implies (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[ )
assume A1: n in dom p ; ::_thesis: (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[
A2: m in NAT by ORDINAL1:def_12;
percases ( r <= 0 or 0 < r ) ;
supposeA3: r <= 0 ; ::_thesis: (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[
then  ].((p /. n) - r),((p /. n) + r).[ = {} ;
hence  (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[ by A3; ::_thesis: verum
end;
supposeA4: 0 < r ; ::_thesis: (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[
A5: dom p = Seg m by FINSEQ_1:89;
thus  (PROJ (m,n)) .: (Ball (p,r)) c= ].((p /. n) - r),((p /. n) + r).[ :: according to XBOOLE_0:def_10 ::_thesis: ].((p /. n) - r),((p /. n) + r).[ c= (PROJ (m,n)) .: (Ball (p,r))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (PROJ (m,n)) .: (Ball (p,r)) or y in ].((p /. n) - r),((p /. n) + r).[ )
assume  y in (PROJ (m,n)) .: (Ball (p,r)) ; ::_thesis: y in ].((p /. n) - r),((p /. n) + r).[
then consider x being Element of (TOP-REAL m) such that
A6: x in Ball (p,r) and
A7: y = (PROJ (m,n)) . x by FUNCT_2:65;
A8: (PROJ (m,n)) . x = x /. n by Def6;
A9: |.(x - p).| < r by A2, A6, TOPREAL9:7;
 0 <= Sum (sqr (x - p)) by RVSUM_1:86;
then  (sqrt (Sum (sqr (x - p)))) ^2 = Sum (sqr (x - p)) by SQUARE_1:def_2;
then A10: Sum (sqr (x - p)) < r ^2 by A9, SQUARE_1:16;
 dom x = Seg m by FINSEQ_1:89;
then  ((x /. n) - (p /. n)) ^2 <= Sum (sqr (x - p)) by A5, A1, EUCLID_9:8;
then  ((x /. n) - (p /. n)) ^2 < r ^2 by A10, XXREAL_0:2;
then  ( - r < (x /. n) - (p /. n) & (x /. n) - (p /. n) < r ) by A4, SQUARE_1:48;
then  ( (- r) + (p /. n) < ((x /. n) - (p /. n)) + (p /. n) & ((x /. n) - (p /. n)) + (p /. n) < r + (p /. n) ) by XREAL_1:6;
hence  y in ].((p /. n) - r),((p /. n) + r).[ by A7, A8, XXREAL_1:4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ].((p /. n) - r),((p /. n) + r).[ or y in (PROJ (m,n)) .: (Ball (p,r)) )
assume A11: y in ].((p /. n) - r),((p /. n) + r).[ ; ::_thesis: y in (PROJ (m,n)) .: (Ball (p,r))
then reconsider y = y as Element of REAL ;
set x = p +* (n,y);
reconsider X = p +* (n,y) as FinSequence of REAL by EUCLID:24;
A12: dom X = dom p by FUNCT_7:30;
A13: p /. n = p . n by A1, PARTFUN1:def_6;
 ( (p /. n) - r < y & y < (p /. n) + r ) by A11, XXREAL_1:4;
then A14: ( y - (p /. n) < r & - r < y - (p /. n) ) by XREAL_1:19, XREAL_1:20;
 (p +* (n,y)) - p = (0* m) +* (n,(y - (p . n))) by Th17;
then  |.((p +* (n,y)) - p).| = abs (y - (p . n)) by A1, A5, Th13;
then  |.((p +* (n,y)) - p).| < r by A13, A14, SEQ_2:1;
then A15: p +* (n,y) in Ball (p,r) by A2, TOPREAL9:7;
(PROJ (m,n)) . (p +* (n,y)) = (p +* (n,y)) /. n by Def6
.= X . n by A12, A1, PARTFUN1:def_6
.= y by A1, FUNCT_7:31 ;
hence  y in (PROJ (m,n)) .: (Ball (p,r)) by A15, FUNCT_2:35; ::_thesis: verum
end;
end;
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
let T be non empty TopSpace; ::_thesis: for m being non zero Nat
for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))
let m be non zero Nat; ::_thesis: for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))
let f be Function of T,R^1; ::_thesis: f = (PROJ (m,m)) * (incl (f,m))
let p be Point of T; :: according to FUNCT_2:def_8 ::_thesis: f . p = ((PROJ (m,m)) * (incl (f,m))) . p
set I = incl (f,m);
reconsider G = m |-> (f . p) as FinSequence of REAL ;
A1: m in NAT by ORDINAL1:def_12;
 1 <= m by NAT_1:14;
then A2: m in Seg m by A1;
A3: dom (m |-> (f . p)) = Seg m by FUNCOP_1:13;
thus ((PROJ (m,m)) * (incl (f,m))) . p = (PROJ (m,m)) . ((incl (f,m)) . p) by FUNCT_2:15
.= ((incl (f,m)) . p) /. m by Def6
.= G /. m by Def4
.= G . m by A2, A3, PARTFUN1:def_6
.= f . p by A2, FINSEQ_2:57 ; ::_thesis: verum
end;

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 & b1 is continuous )
proof
take  T --> (R^1 1) ; ::_thesis: ( T --> (R^1 1) is non-empty & T --> (R^1 1) is continuous )
thus  ( T --> (R^1 1) is non-empty & T --> (R^1 1) is continuous ) ; ::_thesis: verum
end;
end;

theorem :: TOPREALC:57
for n, m being Nat st n in Seg m holds
PROJ (m,n) is continuous
proof
let n, m be Nat; ::_thesis: ( n in Seg m implies PROJ (m,n) is continuous )
assume A1: n in Seg m ; ::_thesis: PROJ (m,n) is continuous
A2: m in NAT by ORDINAL1:def_12;
 for p being Element of (TOP-REAL m) holds (PROJ (m,n)) . p = p /. n by Def6;
hence  PROJ (m,n) is continuous by A2, A1, JORDAN2B:18; ::_thesis: verum
end;

theorem :: TOPREALC:58
for n, m being Nat st n in Seg m holds
PROJ (m,n) is open
proof
let n, m be Nat; ::_thesis: ( n in Seg m implies PROJ (m,n) is open )
set f = PROJ (m,n);
assume A1: n in Seg m ; ::_thesis: PROJ (m,n) is open
 for p being Point of (TOP-REAL m)
for r being positive real number ex s being positive real number st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
proof
let p be Point of (TOP-REAL m); ::_thesis: for r being positive real number ex s being positive real number st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
let r be positive real number ; ::_thesis: ex s being positive real number st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
take  r ; ::_thesis: ].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r))
A2: dom p = Seg m by FINSEQ_1:89;
 p /. n = (PROJ (m,n)) . p by Def6;
hence  ].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r)) by A2, A1, Th55; ::_thesis: verum
end;
hence  PROJ (m,n) is open by TOPS_4:13; ::_thesis: verum
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
reconsider n = n as Element of NAT by ORDINAL1:def_12;
set g = incl (f,n);
percases ( n = 0 or n > 0 ) ;
supposeA1: n = 0 ; ::_thesis: incl (f,n) is continuous
then reconsider z = 0 as Element of (TOP-REAL n) ;
 incl (f,0) = T --> z by Th48;
hence  incl (f,n) is continuous by A1; ::_thesis: verum
end;
supposeA2: n > 0 ; ::_thesis: incl (f,n) is continuous
 for p being Point of T
for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V )
proof
let p be Point of T; ::_thesis: for V being Subset of (TOP-REAL n) st (incl (f,n)) . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V )
let V be Subset of (TOP-REAL n); ::_thesis: ( (incl (f,n)) . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V ) )
assume that
A3: (incl (f,n)) . p in V and
A4: V is open ; ::_thesis: ex W being Subset of T st
( p in W & W is open & (incl (f,n)) .: W c= V )
A5: (incl (f,n)) . p in Int V by A3, A4, TOPS_1:23;
reconsider s = (incl (f,n)) . p as Point of (Euclid n) by EUCLID:67;
consider r being real number  such that
A6: r > 0 and
A7: Ball (s,r) c= V by A5, GOBOARD6:5;
reconsider G = n |-> (f . p) as FinSequence of REAL ;
 1 <= n by A2, NAT_1:14;
then A8: n in Seg n ;
reconsider F = (incl (f,n)) . p as FinSequence of REAL by EUCLID:24;
A9: F = n |-> (f . p) by Def4;
A10: dom (n |-> (f . p)) = Seg n by FUNCOP_1:13;
A11: ((incl (f,n)) . p) /. n = G /. n by Def4
.= G . n by A8, A10, PARTFUN1:def_6
.= f . p by A8, FINSEQ_2:57 ;
set R = r / (sqrt n);
set RR = R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[;
 f . p in R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by A2, A11, A6, TOPREAL6:15;
then consider W being Subset of T such that
A12: ( p in W & W is open ) and
A13: f .: W c= R^1 ].((((incl (f,n)) . p) /. n) - (r / (sqrt n))),((((incl (f,n)) . p) /. n) + (r / (sqrt n))).[ by JGRAPH_2:10;
take  W ; ::_thesis: ( p in W & W is open & (incl (f,n)) .: W c= V )
thus  ( p in W & W is open ) by A12; ::_thesis: (incl (f,n)) .: W c= V
let y be Element of (TOP-REAL n); :: according to LATTICE7:def_1 ::_thesis: ( not y in (incl (f,n)) .: W or y in V )
assume  y in (incl (f,n)) .: W ; ::_thesis: y in V
then consider x being Element of T such that
A14: x in W and
A15: (incl (f,n)) . x = y by FUNCT_2:65;
reconsider y1 = y as Point of (Euclid n) by EUCLID:67;
reconsider y2 = y1, s2 = s as Element of REAL n ;
A16: y2 = n |-> (f . x) by A15, Def4;
A17: (Pitag_dist n) . (y1,s) = |.(y2 - s2).| by EUCLID:def_6
.= (sqrt n) * (abs ((f . x) - (f . p))) by A16, A9, Th11 ;
 f . x in f .: W by A14, FUNCT_2:35;
then  abs ((f . x) - (f . p)) < r / (sqrt n) by A13, A11, RCOMP_1:1;
then  dist (y1,s) < r by A2, A17, XREAL_1:79;
then  y in Ball (s,r) by METRIC_1:11;
hence  y in V by A7; ::_thesis: verum
end;
hence  incl (f,n) is continuous by JGRAPH_2:10; ::_thesis: verum
end;
end;
end;
end;

registration
let n be Nat;
cluster TIMES n ->  continuous ;
coherence
 TIMES n is continuous
proof
percases ( not n is zero or n is zero ) ;
suppose not n is zero ; ::_thesis: TIMES n is continuous
then reconsider n = n as non zero Element of NAT by ORDINAL1:def_12;
set T = TOP-REAL n;
set F = TIMES n;
set J = (Seg n) --> R^1;
set c = the carrier of (TOP-REAL n);
A1: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) by EUCLID_9:28;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider F = TIMES n as Function of [:(TOP-REAL n),(TOP-REAL n):],(product ((Seg n) --> R^1)) by EUCLID_9:28;
A3: the carrier of (TOP-REAL n) = REAL n by EUCLID:22;
now__::_thesis:_for_i_being_Element_of_Seg_n_holds_(proj_(((Seg_n)_-->_R^1),i))_*_F_is_continuous
let i be Element of Seg n; ::_thesis: (proj (((Seg n) --> R^1),i)) * F is continuous
set P = proj (((Seg n) --> R^1),i);
A4: ((Seg n) --> R^1) . i = R^1 by FUNCOP_1:7;
reconsider f = (proj (((Seg n) --> R^1),i)) * F as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by FUNCOP_1:7;
A5: 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;
A6: for a, b being Point of (TOP-REAL n) holds f . (a,b) = (a . i) * (b . i)
proof
let a, b be Point of (TOP-REAL n); ::_thesis: f . (a,b) = (a . i) * (b . i)
thus f . (a,b) = (proj (((Seg n) --> R^1),i)) . (F . (a,b)) by A5, BINOP_1:18
.= (proj (((Seg n) --> R^1),i)) . (a (#) b) by Def5
.= (a (#) b) . i by A1, A2, YELLOW17:8
.= (a . i) * (b . i) by VALUED_1:5 ; ::_thesis: verum
end;
deffunc H1( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) ->  Element of REAL = n . i;
consider f1 being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):],REAL such that
A7: for a, b being Element of the carrier of (TOP-REAL n) holds f1 . (a,b) = H1(a,b) from BINOP_1:sch_4();
reconsider f1 = f1 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;
deffunc H2( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) ->  Element of REAL = c2 . i;
consider f2 being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):],REAL such that
A8: for a, b being Element of the carrier of (TOP-REAL n) holds f2 . (a,b) = H2(a,b) from BINOP_1:sch_4();
reconsider f1 = f1, f2 = f2 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;
 for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r being positive real number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
proof
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for r being positive real number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
let r be positive real number ; ::_thesis: ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
consider p1, p2 being Point of (TOP-REAL n) such that
A9: p = [p1,p2] by BORSUK_1:10;
set B1 = Ball (p1,r);
set B2 = [#] (TOP-REAL n);
reconsider W = [:(Ball (p1,r)),([#] (TOP-REAL n)):] as open Subset of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:6;
take  W ; ::_thesis: ( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
 ( p1 in Ball (p1,r) & p2 in [#] (TOP-REAL n) ) by TOPGEN_5:13;
hence  p in W by A9, ZFMISC_1:def_2; ::_thesis: f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f1 .: W or y in ].((f1 . p) - r),((f1 . p) + r).[ )
assume  y in f1 .: W ; ::_thesis: y in ].((f1 . p) - r),((f1 . p) + r).[
then consider x being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A10: x in W and
A11: f1 . x = y by FUNCT_2:65;
consider x1, x2 being Point of (TOP-REAL n) such that
A12: x = [x1,x2] by BORSUK_1:10;
A13: ( f1 . (x1,x2) = x1 . i & f1 . (p1,p2) = p1 . i ) by A7;
 x1 in Ball (p1,r) by A10, A12, ZFMISC_1:87;
then A14: |.(x1 - p1).| < r by TOPREAL9:7;
 dom (x1 - p1) = Seg n by FINSEQ_1:89;
then  (x1 . i) - (p1 . i) = (x1 - p1) . i by VALUED_1:13;
then  abs ((x1 . i) - (p1 . i)) <= |.(x1 - p1).| by A3, REAL_NS1:8;
then  abs ((f1 . x) - (f1 . p)) < r by A9, A12, A13, A14, XXREAL_0:2;
hence  y in ].((f1 . p) - r),((f1 . p) + r).[ by A11, RCOMP_1:1; ::_thesis: verum
end;
then A15: f1 is continuous by TOPS_4:21;
 for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r being positive real number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
proof
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for r being positive real number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
let r be positive real number ; ::_thesis: ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
consider p1, p2 being Point of (TOP-REAL n) such that
A16: p = [p1,p2] by BORSUK_1:10;
set B1 = [#] (TOP-REAL n);
set B2 = Ball (p2,r);
reconsider W = [:([#] (TOP-REAL n)),(Ball (p2,r)):] as open Subset of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:6;
take  W ; ::_thesis: ( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
 ( p1 in [#] (TOP-REAL n) & p2 in Ball (p2,r) ) by TOPGEN_5:13;
hence  p in W by A16, ZFMISC_1:def_2; ::_thesis: f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f2 .: W or y in ].((f2 . p) - r),((f2 . p) + r).[ )
assume  y in f2 .: W ; ::_thesis: y in ].((f2 . p) - r),((f2 . p) + r).[
then consider x being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A17: x in W and
A18: f2 . x = y by FUNCT_2:65;
consider x1, x2 being Point of (TOP-REAL n) such that
A19: x = [x1,x2] by BORSUK_1:10;
A20: ( f2 . (x1,x2) = x2 . i & f2 . (p1,p2) = p2 . i ) by A8;
 x2 in Ball (p2,r) by A17, A19, ZFMISC_1:87;
then A21: |.(x2 - p2).| < r by TOPREAL9:7;
 dom (x2 - p2) = Seg n by FINSEQ_1:89;
then  (x2 . i) - (p2 . i) = (x2 - p2) . i by VALUED_1:13;
then  abs ((x2 . i) - (p2 . i)) <= |.(x2 - p2).| by A3, REAL_NS1:8;
then  abs ((f2 . x) - (f2 . p)) < r by A16, A19, A20, A21, XXREAL_0:2;
hence  y in ].((f2 . p) - r),((f2 . p) + r).[ by A18, RCOMP_1:1; ::_thesis: verum
end;
then  f2 is continuous by TOPS_4:21;
then consider g being Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 such that
A22: for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 and
A23: g is continuous by A15, JGRAPH_2:25;
now__::_thesis:_for_a,_b_being_Point_of_(TOP-REAL_n)_holds_f_._(a,b)_=_g_._(a,b)
let a, b be Point of (TOP-REAL n); ::_thesis: f . (a,b) = g . (a,b)
A24: ( f1 . (a,b) = a . i & f2 . (a,b) = b . i ) by A7, A8;
thus f . (a,b) = (a . i) * (b . i) by A6
.= g . [a,b] by A22, A24
.= g . (a,b) ; ::_thesis: verum
end;
hence  (proj (((Seg n) --> R^1),i)) * F is continuous by A23, A4, A5, BINOP_1:2; ::_thesis: verum
end;
then  F is continuous by WAYBEL18:6;
hence  TIMES n is continuous by A1, A2, YELLOW12:36; ::_thesis: verum
end;
suppose n is zero ; ::_thesis: TIMES n is continuous
hence  TIMES n is continuous by Th53; ::_thesis: verum
end;
end;
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
let m, n be Nat; ::_thesis: 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)
let f be Function of (TOP-REAL m),(TOP-REAL n); ::_thesis: ( f is continuous implies f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n) )
assume A1: f is continuous ; ::_thesis: f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n)
reconsider g = f (-) as Function of (TOP-REAL m),(TOP-REAL n) by Th34;
 for p being Point of (TOP-REAL m)
for r being positive real number ex s being positive real number st g .: (Ball (p,s)) c= Ball ((g . p),r)
proof
let p be Point of (TOP-REAL m); ::_thesis: for r being positive real number ex s being positive real number st g .: (Ball (p,s)) c= Ball ((g . p),r)
let r be positive real number ; ::_thesis: ex s being positive real number st g .: (Ball (p,s)) c= Ball ((g . p),r)
consider s being positive real number  such that
A2: f .: (Ball ((- p),s)) c= Ball ((f . (- p)),r) by A1, TOPS_4:20;
take  s ; ::_thesis: g .: (Ball (p,s)) c= Ball ((g . p),r)
let y be Element of (TOP-REAL n); :: according to LATTICE7:def_1 ::_thesis: ( not y in g .: (Ball (p,s)) or y in Ball ((g . p),r) )
assume  y in g .: (Ball (p,s)) ; ::_thesis: y in Ball ((g . p),r)
then consider x being Element of (TOP-REAL m) such that
A3: x in Ball (p,s) and
A4: g . x = y by FUNCT_2:65;
 dom g = the carrier of (TOP-REAL m) by FUNCT_2:def_1;
then A5: ( g . x = f . (- x) & g . p = f . (- p) ) by VALUED_2:def_34;
 - x in Ball ((- p),s) by A3, Th23;
then  f . (- x) in f .: (Ball ((- p),s)) by FUNCT_2:35;
hence  y in Ball ((g . p),r) by A2, A4, A5; ::_thesis: verum
end;
hence  f (-) is continuous Function of (TOP-REAL m),(TOP-REAL n) by TOPS_4:20; ::_thesis: verum
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
let F be Function of T,R^1; ::_thesis: ( F = - f implies F is continuous )
assume A1: F = - f ; ::_thesis: F is continuous
consider g being Function of T,R^1 such that
A2: for p being Point of T
for r being real number st f . p = r holds
g . p = - r and
A3: g is continuous by JGRAPH_4:8;
 F = g
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = g . x
thus F . x = - (f . x) by A1, VALUED_1:8
.= g . x by A2 ; ::_thesis: verum
end;
hence  F is continuous by A3; ::_thesis: verum
end;
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
proof
let F be Function of T,R^1; ::_thesis: ( F = f " implies F is continuous )
assume A1: F = f " ; ::_thesis: F is continuous
 dom f = the carrier of T by FUNCT_2:def_1;
then  for q being Point of T holds f . q <> 0 ;
then consider g being Function of T,R^1 such that
A2: for p being Point of T
for r being real number st f . p = r holds
g . p = 1 / r and
A3: g is continuous by JGRAPH_2:26;
 F = g
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = g . x
thus F . x = 1 / (f . x) by A1, VALUED_1:10
.= g . x by A2 ; ::_thesis: verum
end;
hence  F is continuous by A3; ::_thesis: verum
end;
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
proof
let F be Function of T,R^1; ::_thesis: ( F = f + r implies F is continuous )
assume A1: F = f + r ; ::_thesis: F is continuous
consider g being Function of T,R^1 such that
A2: for p being Point of T
for s being real number st f . p = s holds
g . p = s + r and
A3: g is continuous by JGRAPH_2:24;
 F = g
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = g . x
thus F . x = (f . x) + r by A1, VALUED_1:2
.= g . x by A2 ; ::_thesis: verum
end;
hence  F is continuous by A3; ::_thesis: verum
end;
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
proof
let F be Function of T,R^1; ::_thesis: ( F = f (#) r implies F is continuous )
assume A4: F = f (#) r ; ::_thesis: F is continuous
consider g being Function of T,R^1 such that
A5: for p being Point of T
for s being real number st f . p = s holds
g . p = r * s and
A6: g is continuous by JGRAPH_2:23;
 F = g
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = g . x
thus F . x = (f . x) * r by A4, VALUED_1:6
.= g . x by A5 ; ::_thesis: verum
end;
hence  F is continuous by A6; ::_thesis: verum
end;
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
proof
let F be Function of T,R^1; ::_thesis: ( F = f + g implies F is continuous )
assume A1: F = f + g ; ::_thesis: F is continuous
consider h being Function of T,R^1 such that
A2: for p being Point of T
for r1, r2 being real number st f . p = r1 & g . p = r2 holds
h . p = r1 + r2 and
A3: h is continuous by JGRAPH_2:19;
 F = h
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = h . x
thus F . x = (f . x) + (g . x) by A1, VALUED_1:1
.= h . x by A2 ; ::_thesis: verum
end;
hence  F is continuous by A3; ::_thesis: verum
end;
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
proof
 f - g = f + (- g) ;
hence  for b1 being Function of T,R^1 st b1 = f - g holds
b1 is continuous ; ::_thesis: verum
end;
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
proof
let F be Function of T,R^1; ::_thesis: ( F = f (#) g implies F is continuous )
assume A4: F = f (#) g ; ::_thesis: F is continuous
consider h being Function of T,R^1 such that
A5: for p being Point of T
for r1, r2 being real number st f . p = r1 & g . p = r2 holds
h . p = r1 * r2 and
A6: h is continuous by JGRAPH_2:25;
 F = h
proof
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = h . x
thus F . x = (f . x) * (g . x) by A4, VALUED_1:5
.= h . x by A5 ; ::_thesis: verum
end;
hence  F is continuous by A6; ::_thesis: verum
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;
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
proof
 f /" g = f (#) (g ") ;
hence  for b1 being Function of T,R^1 st b1 = f /" g holds
b1 is continuous ; ::_thesis: verum
end;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f <++> g implies h is continuous )
assume A1: h = f <++> g ; ::_thesis: h is continuous
 n in NAT by ORDINAL1:def_12;
then consider F being Function of T,(TOP-REAL n) such that
A2: for r being Point of T holds F . r = (f . r) + (g . r) and
A3: F is continuous by JGRAPH_6:12;
 F = h
proof
A4: dom h = the carrier of T by FUNCT_2:def_1;
let x be Point of T; :: according to FUNCT_2:def_8 ::_thesis: F . x = h . x
thus F . x = (f . x) + (g . x) by A2
.= h . x by A1, A4, VALUED_2:def_45 ; ::_thesis: verum
end;
hence  h is continuous by A3; ::_thesis: verum
end;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f <--> g implies h is continuous )
assume A5: h = f <--> g ; ::_thesis: h is continuous
A6: n in NAT by ORDINAL1:def_12;
A7: for r being Point of T holds h . r = (f . r) - (g . r)
proof
let r be Point of T; ::_thesis: h . r = (f . r) - (g . r)
 dom h = the carrier of T by FUNCT_2:def_1;
hence  h . r = (f . r) - (g . r) by A5, VALUED_2:def_46; ::_thesis: verum
end;
 for p being Point of T
for V being Subset of (TOP-REAL n) st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )
proof
let p be Point of T; ::_thesis: for V being Subset of (TOP-REAL n) st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )
let V be Subset of (TOP-REAL n); ::_thesis: ( h . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & h .: W c= V ) )
assume  ( h . p in V & V is open ) ; ::_thesis: ex W being Subset of T st
( p in W & W is open & h .: W c= V )
then A8: h . p in Int V by TOPS_1:23;
reconsider r = h . p as Point of (Euclid n) by EUCLID:67;
consider r0 being real number  such that
A9: ( r0 > 0 & Ball (r,r0) c= V ) by A8, GOBOARD6:5;
reconsider r01 = f . p as Point of (Euclid n) by EUCLID:67;
reconsider G1 = Ball (r01,(r0 / 2)) as Subset of (TOP-REAL n) by EUCLID:67;
A10: f . p in G1 by A9, GOBOARD6:1;
A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
 G1 is open by A11, TOPMETR:14, TOPS_3:76;
then consider W1 being Subset of T such that
A12: ( p in W1 & W1 is open & f .: W1 c= G1 ) by A10, JGRAPH_2:10;
reconsider r02 = g . p as Point of (Euclid n) by EUCLID:67;
reconsider G2 = Ball (r02,(r0 / 2)) as Subset of (TOP-REAL n) by EUCLID:67;
A13: g . p in G2 by A9, GOBOARD6:1;
 G2 is open by A11, TOPMETR:14, TOPS_3:76;
then consider W2 being Subset of T such that
A14: ( p in W2 & W2 is open & g .: W2 c= G2 ) by A13, JGRAPH_2:10;
take W = W1 /\ W2; ::_thesis: ( p in W & W is open & h .: W c= V )
thus  p in W by A12, A14, XBOOLE_0:def_4; ::_thesis: ( W is open & h .: W c= V )
thus  W is open by A12, A14; ::_thesis: h .: W c= V
let x be Element of (TOP-REAL n); :: according to LATTICE7:def_1 ::_thesis: ( not x in h .: W or x in V )
assume  x in h .: W ; ::_thesis: x in V
then consider z being set  such that
A15: ( z in dom h & z in W & h . z = x ) by FUNCT_1:def_6;
A16: z in W1 by A15, XBOOLE_0:def_4;
reconsider pz = z as Point of T by A15;
 dom f = the carrier of T by FUNCT_2:def_1;
then A17: f . pz in f .: W1 by A16, FUNCT_1:def_6;
reconsider bb1 = f . pz as Point of (Euclid n) by EUCLID:67;
 dist (r01,bb1) < r0 / 2 by A12, A17, METRIC_1:11;
then A18: |.((f . p) - (f . pz)).| < r0 / 2 by A6, JGRAPH_1:28;
A19: z in W2 by A15, XBOOLE_0:def_4;
 dom g = the carrier of T by FUNCT_2:def_1;
then A20: g . pz in g .: W2 by A19, FUNCT_1:def_6;
reconsider bb2 = g . pz as Point of (Euclid n) by EUCLID:67;
 dist (r02,bb2) < r0 / 2 by A14, A20, METRIC_1:11;
then A21: |.((g . p) - (g . pz)).| < r0 / 2 by A6, JGRAPH_1:28;
A22: (f . pz) - (g . pz) = x by A7, A15;
reconsider bb0 = (f . pz) - (g . pz) as Point of (Euclid n) by EUCLID:67;
A23: h . pz = (f . pz) - (g . pz) by A7;
((f . p) - (g . p)) - ((f . pz) - (g . pz)) = (((f . p) - (g . p)) - (f . pz)) + (g . pz) by EUCLID:47
.= (((f . p) + (- (g . p))) + (- (f . pz))) + (g . pz)
.= (((f . p) + (- (f . pz))) + (- (g . p))) + (g . pz) by EUCLID:26
.= (((f . p) - (f . pz)) - (g . p)) + (g . pz)
.= (((f . p) - (f . pz)) + (g . pz)) + (- (g . p)) by EUCLID:26
.= ((f . p) - (f . pz)) + ((g . pz) - (g . p)) by EUCLID:26 ;
then A24: |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| <= |.((f . p) - (f . pz)).| + |.((g . pz) - (g . p)).| by A6, TOPRNS_1:29;
A25: |.((g . p) - (g . pz)).| = |.(- ((g . pz) - (g . p))).| by EUCLID:44
.= |.((g . pz) - (g . p)).| by A6, TOPRNS_1:26 ;
 |.((f . p) - (f . pz)).| + |.((g . p) - (g . pz)).| < (r0 / 2) + (r0 / 2) by A18, A21, XREAL_1:8;
then  |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| < r0 by A24, A25, XXREAL_0:2;
then  |.((h . p) - (h . pz)).| < r0 by A7, A23;
then  dist (r,bb0) < r0 by A6, A15, A22, JGRAPH_1:28;
then  x in Ball (r,r0) by A22, METRIC_1:11;
hence  x in V by A9; ::_thesis: verum
end;
hence  h is continuous by JGRAPH_2:10; ::_thesis: verum
end;
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
proof
A26: f <##> g = (TIMES n) .: (f,g) by Th54;
 <:f,g:> is continuous Function of T,[:(TOP-REAL n),(TOP-REAL n):] by YELLOW12:41;
hence  for b1 being Function of T,(TOP-REAL n) st b1 = f <##> g holds
b1 is continuous by A26; ::_thesis: verum
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);
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f <+> g implies h is continuous )
assume A1: h = f <+> g ; ::_thesis: h is continuous
reconsider G = f <++> (incl (g,n)) as Function of T,(TOP-REAL n) by Th39;
 h = G by A1, Th49;
hence  h is continuous ; ::_thesis: verum
end;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f <-> g implies h is continuous )
assume A2: h = f <-> g ; ::_thesis: h is continuous
reconsider G = f <--> (incl (g,n)) as Function of T,(TOP-REAL n) by Th40;
 h = G by A2, Th50;
hence  h is continuous ; ::_thesis: verum
end;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f <#> g implies h is continuous )
assume A3: h = f <#> g ; ::_thesis: h is continuous
reconsider G = f <##> (incl (g,n)) as Function of T,(TOP-REAL n) by Th41;
 h = G by A3, Th51;
hence  h is continuous ; ::_thesis: verum
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;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f </> g implies h is continuous )
reconsider g1 = g " as Function of T,R^1 ;
 g1 is continuous ;
hence  ( h = f </> g implies h is continuous ) ; ::_thesis: verum
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);
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f [+] r implies h is continuous )
assume A1: h = f [+] r ; ::_thesis: h is continuous
reconsider r = r as Element of R^1 by XREAL_0:def_1;
 dom f = the carrier of T by FUNCT_2:def_1;
then  h = f <+> (T --> r) by A1, Th29;
hence  h is continuous ; ::_thesis: verum
end;
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
proof
let h be Function of T,(TOP-REAL n); ::_thesis: ( h = f [#] r implies h is continuous )
assume A2: h = f [#] r ; ::_thesis: h is continuous
reconsider r = r as Element of R^1 by XREAL_0:def_1;
 dom f = the carrier of T by FUNCT_2:def_1;
then  h = f <#> (T --> r) by A2, Th31;
hence  h is continuous ; ::_thesis: verum
end;
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))
proof
let r be non negative real number ; ::_thesis: 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))
let n be non zero Nat; ::_thesis: for p being Point of (Tcircle ((0. (TOP-REAL n)),r)) holds - p is Point of (Tcircle ((0. (TOP-REAL n)),r))
let p be Point of (Tcircle ((0. (TOP-REAL n)),r)); ::_thesis: - p is Point of (Tcircle ((0. (TOP-REAL n)),r))
reconsider p1 = p as Point of (TOP-REAL n) by PRE_TOPC:25;
A1: n in NAT by ORDINAL1:def_12;
then A2: the carrier of (Tcircle ((0. (TOP-REAL n)),r)) = Sphere ((0. (TOP-REAL n)),r) by TOPREALB:9;
|.((- p1) - (0. (TOP-REAL n))).| = |.(- p1).| by RLVECT_1:13
.= |.p1.| by EUCLID:71
.= |.(p1 - (0. (TOP-REAL n))).| by RLVECT_1:13
.= r by A1, A2, TOPREAL9:9 ;
hence  - p is Point of (Tcircle ((0. (TOP-REAL n)),r)) by A2, A1, TOPREAL9:9; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_thesis: 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)
let r be non negative real number ; ::_thesis: 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)
set X = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r));
let f be Function of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n); ::_thesis: f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n)
set g = f (-) ;
A1: dom (f (-)) = dom f by VALUED_2:def_34;
A2: dom f = the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by FUNCT_2:def_1;
 for x being set st x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) holds
(f (-)) . x in the carrier of (TOP-REAL n)
proof
let x be set ; ::_thesis: ( x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) implies (f (-)) . x in the carrier of (TOP-REAL n) )
assume  x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; ::_thesis: (f (-)) . x in the carrier of (TOP-REAL n)
then reconsider x = x as Element of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ;
reconsider y = - x as Element of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by Th60;
reconsider f = f as Function of the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n) ;
 (f (-)) . x = f . y by A1, A2, VALUED_2:def_34;
hence  (f (-)) . x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence  f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n) by A1, A2, FUNCT_2:3; ::_thesis: verum
end;

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))
proof
set T = Tcircle ((0. (TOP-REAL (n + 1))),r);
 (-) X c= the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (-) X or x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) )
assume A1: x in (-) X ; ::_thesis: x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))
then reconsider x = x as Element of (-) X ;
 - x in X by A1, Th24;
then  - (- x) is Point of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by Th60;
hence  x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; ::_thesis: verum
end;
hence  (-) X is Subset of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; ::_thesis: verum
end;
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
proof
set T = Tcircle ((0. (TOP-REAL (m + 1))),r);
 ex G being Subset of (TOP-REAL (m + 1)) st
( G is open & (-) X = G /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
proof
consider G being Subset of (TOP-REAL (m + 1)) such that
A1: G is open and
A2: X = G /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by TSP_1:def_1;
take  (-) G ; ::_thesis: ( (-) G is open & (-) X = ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
thus  (-) G is open by A1; ::_thesis: (-) X = ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r))
thus  (-) X c= ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) :: according to XBOOLE_0:def_10 ::_thesis: ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) c= (-) X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (-) X or x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
assume A3: x in (-) X ; ::_thesis: x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r))
then reconsider x = x as Element of (-) X ;
 - x in X by A3, Th24;
then  - x in G by A2, XBOOLE_0:def_4;
then  x in (-) G by Th24;
hence  x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) or x in (-) X )
assume A4: x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) ; ::_thesis: x in (-) X
then reconsider x = x as Element of (-) G by XBOOLE_0:def_4;
 x in (-) G by A4, XBOOLE_0:def_4;
then A5: - x in G by Th24;
 x in the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by A4, XBOOLE_0:def_4;
then  - x is Point of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by Th60;
then  - x in X by A2, A5, XBOOLE_0:def_4;
hence  x in (-) X by Th24; ::_thesis: verum
end;
hence  for b1 being Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st b1 = (-) X holds
b1 is open by TSP_1:def_1; ::_thesis: verum
end;
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)
proof
let m be Nat; ::_thesis: 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)
let r be non negative real number ; ::_thesis: 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)
set T = Tcircle ((0. (TOP-REAL (m + 1))),r);
let f be continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(TOP-REAL m); ::_thesis: f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(TOP-REAL m)
reconsider g = f (-) as Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(TOP-REAL m) by Th61;
 for p being Point of (Tcircle ((0. (TOP-REAL (m + 1))),r))
for r being positive real number ex W being open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st
( p in W & g .: W c= Ball ((g . p),r) )
proof
let p be Point of (Tcircle ((0. (TOP-REAL (m + 1))),r)); ::_thesis: for r being positive real number ex W being open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st
( p in W & g .: W c= Ball ((g . p),r) )
let r be positive real number ; ::_thesis: ex W being open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st
( p in W & g .: W c= Ball ((g . p),r) )
reconsider q = - p as Point of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by Th60;
consider W being open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) such that
A1: q in W and
A2: f .: W c= Ball ((f . q),r) by TOPS_4:18;
reconsider W1 = (-) W as open Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) ;
take  W1 ; ::_thesis: ( p in W1 & g .: W1 c= Ball ((g . p),r) )
 - q in W1 by A1, Def3;
hence  p in W1 ; ::_thesis: g .: W1 c= Ball ((g . p),r)
let y be Element of (TOP-REAL m); :: according to LATTICE7:def_1 ::_thesis: ( not y in g .: W1 or y in Ball ((g . p),r) )
assume  y in g .: W1 ; ::_thesis: y in Ball ((g . p),r)
then consider x being Element of (Tcircle ((0. (TOP-REAL (m + 1))),r)) such that
A3: x in W1 and
A4: g . x = y by FUNCT_2:65;
 dom g = the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by FUNCT_2:def_1;
then A5: ( g . x = f . (- x) & g . p = f . (- p) ) by VALUED_2:def_34;
 - x in (-) W1 by A3, Def3;
then  f . (- x) in f .: W by FUNCT_2:35;
hence  y in Ball ((g . p),r) by A2, A4, A5; ::_thesis: verum
end;
hence  f (-) is continuous Function of (Tcircle ((0. (TOP-REAL (m + 1))),r)),(TOP-REAL m) by TOPS_4:18; ::_thesis: verum
end;