:: NCFCONT1 semantic presentation

definition

let c₁ be ComplexLinearSpace;
let c₂ be sequence of c₁;
func - c₂ -> sequence of a₁ means :Def1: :: NCFCONT1:def 1
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines - NCFCONT1:def 1 :

theorem Th1: :: NCFCONT1:1

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ holds b₂ - b₃ = b₂ + (- b₃)

proof end;

theorem Th2: :: NCFCONT1:2

for b₁ being ComplexNormSpace
for b₂ being sequence of b₁ holds - b₂ = (- 1r ) * b₂

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
func ||.c₃.|| -> PartFunc of the carrier of a₁, REAL means :Def2: :: NCFCONT1:def 2
( dom a₄ = dom a₃ & ( for b₁ being Point of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ||. NCFCONT1:def 2 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
func ||.c₃.|| -> PartFunc of the carrier of a₁, REAL means :Def3: :: NCFCONT1:def 3
( dom a₄ = dom a₃ & ( for b₁ being Point of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ||. NCFCONT1:def 3 :

definition

let c₁ be RealNormSpace;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
func ||.c₃.|| -> PartFunc of the carrier of a₁, REAL means :Def4: :: NCFCONT1:def 4
( dom a₄ = dom a₃ & ( for b₁ being Point of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ||. NCFCONT1:def 4 :

definition

let c₁ be ComplexNormSpace;
let c₂ be Point of c₁;
mode Neighbourhood of c₂ -> Subset of a₁ means :Def5: :: NCFCONT1:def 5
ex b₁ being Real st
( 0 < b₁ & { b₂ where B is Point of a₁ : ||.(b₂ - a₂).|| < b₁ } c= a₃ );
existence

proof end;

end;

:: deftheorem Def5 defines Neighbourhood NCFCONT1:def 5 :

theorem Th3: :: NCFCONT1:3

for b₁ being ComplexNormSpace
for b₂ being Point of b₁
for b₃ being Real st 0 < b₃ holds
{ b₄ where B is Point of b₁ : ||.(b₄ - b₂).|| < b₃ } is Neighbourhood of b₂

proof end;

theorem Th4: :: NCFCONT1:4

for b₁ being ComplexNormSpace
for b₂ being Point of b₁
for b₃ being Neighbourhood of b₂ holds b₂ in b₃

proof end;

definition

let c₁ be ComplexNormSpace;
let c₂ be Subset of c₁;
attr a₂ is compact means :Def6: :: NCFCONT1:def 6
for b₁ being sequence of a₁ st rng b₁ c= a₂ holds
ex b₂ being sequence of a₁ st
( b₂ is subsequence of b₁ & b₂ is convergent & lim b₂ in a₂ );

end;

:: deftheorem Def6 defines compact NCFCONT1:def 6 :

definition

let c₁ be ComplexNormSpace;
let c₂ be Subset of c₁;
attr a₂ is closed means :: NCFCONT1:def 7
for b₁ being sequence of a₁ st rng b₁ c= a₂ & b₁ is convergent holds
lim b₁ in a₂;

end;

:: deftheorem Def7 defines closed NCFCONT1:def 7 :

definition

let c₁ be ComplexNormSpace;
let c₂ be Subset of c₁;
attr a₂ is open means :: NCFCONT1:def 8
a₂ ` is closed;

end;

:: deftheorem Def8 defines open NCFCONT1:def 8 :

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be sequence of c₁;
assume E10: rng c₄ c= dom c₃ ;
func c₃ * c₄ -> sequence of a₂ equals :Def9: :: NCFCONT1:def 9
a₃ * a₄;
coherence

proof end;

end;

:: deftheorem Def9 defines * NCFCONT1:def 9 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be sequence of c₁;
assume E11: rng c₄ c= dom c₃ ;
func c₃ * c₄ -> sequence of a₂ equals :Def10: :: NCFCONT1:def 10
a₃ * a₄;
coherence

proof end;

end;

:: deftheorem Def10 defines * NCFCONT1:def 10 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₂,c₁;
let c₄ be sequence of c₂;
assume E12: rng c₄ c= dom c₃ ;
func c₃ * c₄ -> sequence of a₁ equals :Def11: :: NCFCONT1:def 11
a₃ * a₄;
coherence

proof end;

end;

:: deftheorem Def11 defines * NCFCONT1:def 11 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be sequence of c₁;
assume E13: rng c₃ c= dom c₂ ;
func c₂ * c₃ -> Complex_Sequence equals :Def12: :: NCFCONT1:def 12
a₂ * a₃;
coherence

proof end;

end;

:: deftheorem Def12 defines * NCFCONT1:def 12 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be sequence of c₁;
assume E14: rng c₃ c= dom c₂ ;
func c₂ * c₃ -> Complex_Sequence equals :Def13: :: NCFCONT1:def 13
a₂ * a₃;
coherence

proof end;

end;

:: deftheorem Def13 defines * NCFCONT1:def 13 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be sequence of c₁;
assume E15: rng c₃ c= dom c₂ ;
func c₂ * c₃ -> Real_Sequence equals :Def14: :: NCFCONT1:def 14
a₂ * a₃;
coherence

proof end;

end;

:: deftheorem Def14 defines * NCFCONT1:def 14 :

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be Point of c₁;
pred c₃ is_continuous_in c₄ means :Def15: :: NCFCONT1:def 15
( a₄ in dom a₃ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₃ & b₁ is convergent & lim b₁ = a₄ holds
( a₃ * b₁ is convergent & a₃ /. a₄ = lim (a₃ * b₁) ) ) );

end;

:: deftheorem Def15 defines is_continuous_in NCFCONT1:def 15 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be Point of c₁;
pred c₃ is_continuous_in c₄ means :Def16: :: NCFCONT1:def 16
( a₄ in dom a₃ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₃ & b₁ is convergent & lim b₁ = a₄ holds
( a₃ * b₁ is convergent & a₃ /. a₄ = lim (a₃ * b₁) ) ) );

end;

:: deftheorem Def16 defines is_continuous_in NCFCONT1:def 16 :

definition

let c₁ be RealNormSpace;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be Point of c₁;
pred c₃ is_continuous_in c₄ means :Def17: :: NCFCONT1:def 17
( a₄ in dom a₃ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₃ & b₁ is convergent & lim b₁ = a₄ holds
( a₃ * b₁ is convergent & a₃ /. a₄ = lim (a₃ * b₁) ) ) );

end;

:: deftheorem Def17 defines is_continuous_in NCFCONT1:def 17 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be Point of c₁;
pred c₂ is_continuous_in c₃ means :Def18: :: NCFCONT1:def 18
( a₃ in dom a₂ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₂ & b₁ is convergent & lim b₁ = a₃ holds
( a₂ * b₁ is convergent & a₂ /. a₃ = lim (a₂ * b₁) ) ) );

end;

:: deftheorem Def18 defines is_continuous_in NCFCONT1:def 18 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be Point of c₁;
pred c₂ is_continuous_in c₃ means :Def19: :: NCFCONT1:def 19
( a₃ in dom a₂ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₂ & b₁ is convergent & lim b₁ = a₃ holds
( a₂ * b₁ is convergent & a₂ /. a₃ = lim (a₂ * b₁) ) ) );

end;

:: deftheorem Def19 defines is_continuous_in NCFCONT1:def 19 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be Point of c₁;
pred c₂ is_continuous_in c₃ means :Def20: :: NCFCONT1:def 20
( a₃ in dom a₂ & ( for b₁ being sequence of a₁ st rng b₁ c= dom a₂ & b₁ is convergent & lim b₁ = a₃ holds
( a₂ * b₁ is convergent & a₂ /. a₃ = lim (a₂ * b₁) ) ) );

end;

:: deftheorem Def20 defines is_continuous_in NCFCONT1:def 20 :

theorem Th5: :: NCFCONT1:5

for b₁ being Nat
for b₂, b₃ being ComplexNormSpace
for b₄ being sequence of b₂
for b₅ being PartFunc of b₂,b₃ st rng b₄ c= dom b₅ holds
b₄ . b₁ in dom b₅

proof end;

theorem Th6: :: NCFCONT1:6

for b₁ being Nat
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being sequence of b₂
for b₅ being PartFunc of b₂,b₃ st rng b₄ c= dom b₅ holds
b₄ . b₁ in dom b₅

proof end;

theorem Th7: :: NCFCONT1:7

for b₁ being Nat
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being sequence of b₃
for b₅ being PartFunc of b₃,b₂ st rng b₄ c= dom b₅ holds
b₄ . b₁ in dom b₅

proof end;

theorem Th8: :: NCFCONT1:8

for b₁ being ComplexNormSpace
for b₂ being sequence of b₁
for b₃ being set holds
( b₃ in rng b₂ iff ex b₄ being Nat st b₃ = b₂ . b₄ )

proof end;

theorem Th9: :: NCFCONT1:9

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ st b₃ is subsequence of b₂ holds
rng b₃ c= rng b₂

proof end;

theorem Th10: :: NCFCONT1:10

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁ st rng b₄ c= dom b₃ holds
for b₅ being Nat holds (b₃ * b₄) . b₅ = b₃ /. (b₄ . b₅)

proof end;

theorem Th11: :: NCFCONT1:11

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁ st rng b₄ c= dom b₃ holds
for b₅ being Nat holds (b₃ * b₄) . b₅ = b₃ /. (b₄ . b₅)

proof end;

theorem Th12: :: NCFCONT1:12

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being sequence of b₂ st rng b₄ c= dom b₃ holds
for b₅ being Nat holds (b₃ * b₄) . b₅ = b₃ /. (b₄ . b₅)

proof end;

theorem Th13: :: NCFCONT1:13

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being sequence of b₁ st rng b₃ c= dom b₂ holds
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ /. (b₃ . b₄)

proof end;

theorem Th14: :: NCFCONT1:14

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being sequence of b₁ st rng b₃ c= dom b₂ holds
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ /. (b₃ . b₄)

proof end;

theorem Th15: :: NCFCONT1:15

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being sequence of b₁ st rng b₃ c= dom b₂ holds
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ /. (b₃ . b₄)

proof end;

theorem Th16: :: NCFCONT1:16

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being increasing Seq_of_Nat st rng b₄ c= dom b₃ holds
(b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th17: :: NCFCONT1:17

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being increasing Seq_of_Nat st rng b₄ c= dom b₃ holds
(b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th18: :: NCFCONT1:18

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being sequence of b₂
for b₅ being increasing Seq_of_Nat st rng b₄ c= dom b₃ holds
(b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th19: :: NCFCONT1:19

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being sequence of b₁
for b₄ being increasing Seq_of_Nat st rng b₃ c= dom b₂ holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th20: :: NCFCONT1:20

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being sequence of b₁
for b₄ being increasing Seq_of_Nat st rng b₃ c= dom b₂ holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th21: :: NCFCONT1:21

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being sequence of b₁
for b₄ being increasing Seq_of_Nat st rng b₃ c= dom b₂ holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th22: :: NCFCONT1:22

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄, b₅ being sequence of b₁ st rng b₄ c= dom b₃ & b₅ is subsequence of b₄ holds
b₃ * b₅ is subsequence of b₃ * b₄

proof end;

theorem Th23: :: NCFCONT1:23

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄, b₅ being sequence of b₁ st rng b₄ c= dom b₃ & b₅ is subsequence of b₄ holds
b₃ * b₅ is subsequence of b₃ * b₄

proof end;

theorem Th24: :: NCFCONT1:24

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄, b₅ being sequence of b₂ st rng b₄ c= dom b₃ & b₅ is subsequence of b₄ holds
b₃ * b₅ is subsequence of b₃ * b₄

proof end;

theorem Th25: :: NCFCONT1:25

for b₁ being Complex_Sequence
for b₂ being Nat
for b₃ being increasing Seq_of_Nat holds (b₁ * b₃) . b₂ = b₁ . (b₃ . b₂)

proof end;

theorem Th26: :: NCFCONT1:26

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃, b₄ being sequence of b₁ st rng b₃ c= dom b₂ & b₄ is subsequence of b₃ holds
b₂ * b₄ is subsequence of b₂ * b₃

proof end;

theorem Th27: :: NCFCONT1:27

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃, b₄ being sequence of b₁ st rng b₃ c= dom b₂ & b₄ is subsequence of b₃ holds
b₂ * b₄ is subsequence of b₂ * b₃

proof end;

theorem Th28: :: NCFCONT1:28

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃, b₄ being sequence of b₁ st rng b₃ c= dom b₂ & b₄ is subsequence of b₃ holds
b₂ * b₄ is subsequence of b₂ * b₃

proof end;

theorem Th29: :: NCFCONT1:29

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Real st 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₁ st b₇ in dom b₃ & ||.(b₇ - b₄).|| < b₆ holds
||.((b₃ /. b₇) - (b₃ /. b₄)).|| < b₅ ) ) ) ) )

proof end;

theorem Th30: :: NCFCONT1:30

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Real st 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₁ st b₇ in dom b₃ & ||.(b₇ - b₄).|| < b₆ holds
||.((b₃ /. b₇) - (b₃ /. b₄)).|| < b₅ ) ) ) ) )

proof end;

theorem Th31: :: NCFCONT1:31

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Real st 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₂ st b₇ in dom b₃ & ||.(b₇ - b₄).|| < b₆ holds
||.((b₃ /. b₇) - (b₃ /. b₄)).|| < b₅ ) ) ) ) )

proof end;

theorem Th32: :: NCFCONT1:32

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being Point of b₁ holds
( b₂ is_continuous_in b₃ iff ( b₃ in dom b₂ & ( for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Point of b₁ st b₆ in dom b₂ & ||.(b₆ - b₃).|| < b₅ holds
abs ((b₂ /. b₆) - (b₂ /. b₃)) < b₄ ) ) ) ) )

proof end;

theorem Th33: :: NCFCONT1:33

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being Point of b₁ holds
( b₂ is_continuous_in b₃ iff ( b₃ in dom b₂ & ( for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Point of b₁ st b₆ in dom b₂ & ||.(b₆ - b₃).|| < b₅ holds
|.((b₂ /. b₆) - (b₂ /. b₃)).| < b₄ ) ) ) ) )

proof end;

theorem Th34: :: NCFCONT1:34

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX
for b₃ being Point of b₁ holds
( b₂ is_continuous_in b₃ iff ( b₃ in dom b₂ & ( for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Point of b₁ st b₆ in dom b₂ & ||.(b₆ - b₃).|| < b₅ holds
|.((b₂ /. b₆) - (b₂ /. b₃)).| < b₄ ) ) ) ) )

proof end;

theorem Th35: :: NCFCONT1:35

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Neighbourhood of b₃ /. b₄ ex b₆ being Neighbourhood of b₄ st
for b₇ being Point of b₁ st b₇ in dom b₃ & b₇ in b₆ holds
b₃ /. b₇ in b₅ ) ) )

proof end;

theorem Th36: :: NCFCONT1:36

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Neighbourhood of b₃ /. b₄ ex b₆ being Neighbourhood of b₄ st
for b₇ being Point of b₁ st b₇ in dom b₃ & b₇ in b₆ holds
b₃ /. b₇ in b₅ ) ) )

proof end;

theorem Th37: :: NCFCONT1:37

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ holds
( b₃ is_continuous_in b₄ iff ( b₄ in dom b₃ & ( for b₅ being Neighbourhood of b₃ /. b₄ ex b₆ being Neighbourhood of b₄ st
for b₇ being Point of b₂ st b₇ in dom b₃ & b₇ in b₆ holds
b₃ /. b₇ in b₅ ) ) )

proof end;

theorem Th38: :: NCFCONT1:38

proof end;

theorem Th39: :: NCFCONT1:39

proof end;

theorem Th40: :: NCFCONT1:40

proof end;

theorem Th41: :: NCFCONT1:41

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₄ in dom b₃ & ex b₅ being Neighbourhood of b₄ st (dom b₃) /\ b₅ = {b₄} holds
b₃ is_continuous_in b₄

proof end;

theorem Th42: :: NCFCONT1:42

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₄ in dom b₃ & ex b₅ being Neighbourhood of b₄ st (dom b₃) /\ b₅ = {b₄} holds
b₃ is_continuous_in b₄

proof end;

theorem Th43: :: NCFCONT1:43

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₄ in dom b₃ & ex b₅ being Neighbourhood of b₄ st (dom b₃) /\ b₅ = {b₄} holds
b₃ is_continuous_in b₄

proof end;

theorem Th44: :: NCFCONT1:44

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being sequence of b₁ st rng b₅ c= (dom b₃) /\ (dom b₄) holds
( (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅) & (b₃ - b₄) * b₅ = (b₃ * b₅) - (b₄ * b₅) )

proof end;

theorem Th45: :: NCFCONT1:45

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being sequence of b₁ st rng b₅ c= (dom b₃) /\ (dom b₄) holds
( (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅) & (b₃ - b₄) * b₅ = (b₃ * b₅) - (b₄ * b₅) )

proof end;

theorem Th46: :: NCFCONT1:46

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₂,b₁
for b₅ being sequence of b₂ st rng b₅ c= (dom b₃) /\ (dom b₄) holds
( (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅) & (b₃ - b₄) * b₅ = (b₃ * b₅) - (b₄ * b₅) )

proof end;

theorem Th47: :: NCFCONT1:47

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being Complex st rng b₄ c= dom b₃ holds
(b₅ (#) b₃) * b₄ = b₅ * (b₃ * b₄)

proof end;

theorem Th48: :: NCFCONT1:48

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁
for b₅ being Real st rng b₄ c= dom b₃ holds
(b₅ (#) b₃) * b₄ = b₅ * (b₃ * b₄)

proof end;

theorem Th49: :: NCFCONT1:49

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being sequence of b₂
for b₅ being Complex st rng b₄ c= dom b₃ holds
(b₅ (#) b₃) * b₄ = b₅ * (b₃ * b₄)

proof end;

theorem Th50: :: NCFCONT1:50

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁ st rng b₄ c= dom b₃ holds
( ||.(b₃ * b₄).|| = ||.b₃.|| * b₄ & - (b₃ * b₄) = (- b₃) * b₄ )

proof end;

theorem Th51: :: NCFCONT1:51

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being sequence of b₁ st rng b₄ c= dom b₃ holds
( ||.(b₃ * b₄).|| = ||.b₃.|| * b₄ & - (b₃ * b₄) = (- b₃) * b₄ )

proof end;

theorem Th52: :: NCFCONT1:52

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being sequence of b₂ st rng b₄ c= dom b₃ holds
( ||.(b₃ * b₄).|| = ||.b₃.|| * b₄ & - (b₃ * b₄) = (- b₃) * b₄ )

proof end;

theorem Th53: :: NCFCONT1:53

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being Point of b₁ st b₃ is_continuous_in b₅ & b₄ is_continuous_in b₅ holds
( b₃ + b₄ is_continuous_in b₅ & b₃ - b₄ is_continuous_in b₅ )

proof end;

theorem Th54: :: NCFCONT1:54

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being Point of b₁ st b₃ is_continuous_in b₅ & b₄ is_continuous_in b₅ holds
( b₃ + b₄ is_continuous_in b₅ & b₃ - b₄ is_continuous_in b₅ )

proof end;

theorem Th55: :: NCFCONT1:55

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being PartFunc of b₂,b₁
for b₅ being Point of b₂ st b₃ is_continuous_in b₅ & b₄ is_continuous_in b₅ holds
( b₃ + b₄ is_continuous_in b₅ & b₃ - b₄ is_continuous_in b₅ )

proof end;

theorem Th56: :: NCFCONT1:56

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁
for b₅ being Complex st b₃ is_continuous_in b₄ holds
b₅ (#) b₃ is_continuous_in b₄

proof end;

theorem Th57: :: NCFCONT1:57

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁
for b₅ being Real st b₃ is_continuous_in b₄ holds
b₅ (#) b₃ is_continuous_in b₄

proof end;

theorem Th58: :: NCFCONT1:58

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂
for b₅ being Complex st b₃ is_continuous_in b₄ holds
b₅ (#) b₃ is_continuous_in b₄

proof end;

theorem Th59: :: NCFCONT1:59

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₃ is_continuous_in b₄ holds
( ||.b₃.|| is_continuous_in b₄ & - b₃ is_continuous_in b₄ )

proof end;

theorem Th60: :: NCFCONT1:60

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₃ is_continuous_in b₄ holds
( ||.b₃.|| is_continuous_in b₄ & - b₃ is_continuous_in b₄ )

proof end;

theorem Th61: :: NCFCONT1:61

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₃ is_continuous_in b₄ holds
( ||.b₃.|| is_continuous_in b₄ & - b₃ is_continuous_in b₄ )

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
pred c₃ is_continuous_on c₄ means :Def21: :: NCFCONT1:def 21
( a₄ c= dom a₃ & ( for b₁ being Point of a₁ st b₁ in a₄ holds
a₃ | a₄ is_continuous_in b₁ ) );

end;

:: deftheorem Def21 defines is_continuous_on NCFCONT1:def 21 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
pred c₃ is_continuous_on c₄ means :Def22: :: NCFCONT1:def 22
( a₄ c= dom a₃ & ( for b₁ being Point of a₁ st b₁ in a₄ holds
a₃ | a₄ is_continuous_in b₁ ) );

end;

:: deftheorem Def22 defines is_continuous_on NCFCONT1:def 22 :

definition

let c₁ be RealNormSpace;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
pred c₃ is_continuous_on c₄ means :Def23: :: NCFCONT1:def 23
( a₄ c= dom a₃ & ( for b₁ being Point of a₁ st b₁ in a₄ holds
a₃ | a₄ is_continuous_in b₁ ) );

end;

:: deftheorem Def23 defines is_continuous_on NCFCONT1:def 23 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be set ;
pred c₂ is_continuous_on c₃ means :Def24: :: NCFCONT1:def 24
( a₃ c= dom a₂ & ( for b₁ being Point of a₁ st b₁ in a₃ holds
a₂ | a₃ is_continuous_in b₁ ) );

end;

:: deftheorem Def24 defines is_continuous_on NCFCONT1:def 24 :

definition

let c₁ be ComplexNormSpace;
let c₂ be PartFunc of the carrier of c₁, REAL ;
let c₃ be set ;
pred c₂ is_continuous_on c₃ means :Def25: :: NCFCONT1:def 25
( a₃ c= dom a₂ & ( for b₁ being Point of a₁ st b₁ in a₃ holds
a₂ | a₃ is_continuous_in b₁ ) );

end;

:: deftheorem Def25 defines is_continuous_on NCFCONT1:def 25 :

definition

let c₁ be RealNormSpace;
let c₂ be PartFunc of the carrier of c₁, COMPLEX ;
let c₃ be set ;
pred c₂ is_continuous_on c₃ means :Def26: :: NCFCONT1:def 26
( a₃ c= dom a₂ & ( for b₁ being Point of a₁ st b₁ in a₃ holds
a₂ | a₃ is_continuous_in b₁ ) );

end;

:: deftheorem Def26 defines is_continuous_on NCFCONT1:def 26 :

theorem Th62: :: NCFCONT1:62

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being sequence of b₁ st rng b₅ c= b₃ & b₅ is convergent & lim b₅ in b₃ holds
( b₄ * b₅ is convergent & b₄ /. (lim b₅) = lim (b₄ * b₅) ) ) ) )

proof end;

theorem Th63: :: NCFCONT1:63

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being sequence of b₁ st rng b₅ c= b₃ & b₅ is convergent & lim b₅ in b₃ holds
( b₄ * b₅ is convergent & b₄ /. (lim b₅) = lim (b₄ * b₅) ) ) ) )

proof end;

theorem Th64: :: NCFCONT1:64

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being sequence of b₂ st rng b₅ c= b₃ & b₅ is convergent & lim b₅ in b₃ holds
( b₄ * b₅ is convergent & b₄ /. (lim b₅) = lim (b₄ * b₅) ) ) ) )

proof end;

theorem Th65: :: NCFCONT1:65

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being Point of b₁
for b₆ being Real st b₅ in b₃ & 0 < b₆ holds
ex b₇ being Real st
( 0 < b₇ & ( for b₈ being Point of b₁ st b₈ in b₃ & ||.(b₈ - b₅).|| < b₇ holds
||.((b₄ /. b₈) - (b₄ /. b₅)).|| < b₆ ) ) ) ) )

proof end;

theorem Th66: :: NCFCONT1:66

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being Point of b₁
for b₆ being Real st b₅ in b₃ & 0 < b₆ holds
ex b₇ being Real st
( 0 < b₇ & ( for b₈ being Point of b₁ st b₈ in b₃ & ||.(b₈ - b₅).|| < b₇ holds
||.((b₄ /. b₈) - (b₄ /. b₅)).|| < b₆ ) ) ) ) )

proof end;

theorem Th67: :: NCFCONT1:67

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ holds
( b₄ is_continuous_on b₃ iff ( b₃ c= dom b₄ & ( for b₅ being Point of b₂
for b₆ being Real st b₅ in b₃ & 0 < b₆ holds
ex b₇ being Real st
( 0 < b₇ & ( for b₈ being Point of b₂ st b₈ in b₃ & ||.(b₈ - b₅).|| < b₇ holds
||.((b₄ /. b₈) - (b₄ /. b₅)).|| < b₆ ) ) ) ) )

proof end;

theorem Th68: :: NCFCONT1:68

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX holds
( b₃ is_continuous_on b₂ iff ( b₂ c= dom b₃ & ( for b₄ being Point of b₁
for b₅ being Real st b₄ in b₂ & 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₁ st b₇ in b₂ & ||.(b₇ - b₄).|| < b₆ holds
|.((b₃ /. b₇) - (b₃ /. b₄)).| < b₅ ) ) ) ) )

proof end;

theorem Th69: :: NCFCONT1:69

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, REAL holds
( b₃ is_continuous_on b₂ iff ( b₂ c= dom b₃ & ( for b₄ being Point of b₁
for b₅ being Real st b₄ in b₂ & 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₁ st b₇ in b₂ & ||.(b₇ - b₄).|| < b₆ holds
abs ((b₃ /. b₇) - (b₃ /. b₄)) < b₅ ) ) ) ) )

proof end;

theorem Th70: :: NCFCONT1:70

for b₁ being RealNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX holds
( b₃ is_continuous_on b₂ iff ( b₂ c= dom b₃ & ( for b₄ being Point of b₁
for b₅ being Real st b₄ in b₂ & 0 < b₅ holds
ex b₆ being Real st
( 0 < b₆ & ( for b₇ being Point of b₁ st b₇ in b₂ & ||.(b₇ - b₄).|| < b₆ holds
|.((b₃ /. b₇) - (b₃ /. b₄)).| < b₅ ) ) ) ) )

proof end;

theorem Th71: :: NCFCONT1:71

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff b₄ | b₃ is_continuous_on b₃ )

proof end;

theorem Th72: :: NCFCONT1:72

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds
( b₄ is_continuous_on b₃ iff b₄ | b₃ is_continuous_on b₃ )

proof end;

theorem Th73: :: NCFCONT1:73

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ holds
( b₄ is_continuous_on b₃ iff b₄ | b₃ is_continuous_on b₃ )

proof end;

theorem Th74: :: NCFCONT1:74

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX holds
( b₃ is_continuous_on b₂ iff b₃ | b₂ is_continuous_on b₂ )

proof end;

theorem Th75: :: NCFCONT1:75

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, REAL holds
( b₃ is_continuous_on b₂ iff b₃ | b₂ is_continuous_on b₂ )

proof end;

theorem Th76: :: NCFCONT1:76

for b₁ being RealNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX holds
( b₃ is_continuous_on b₂ iff b₃ | b₂ is_continuous_on b₂ )

proof end;

theorem Th77: :: NCFCONT1:77

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₁,b₂ st b₅ is_continuous_on b₃ & b₄ c= b₃ holds
b₅ is_continuous_on b₄

proof end;

theorem Th78: :: NCFCONT1:78

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₁,b₂ st b₅ is_continuous_on b₃ & b₄ c= b₃ holds
b₅ is_continuous_on b₄

proof end;

theorem Th79: :: NCFCONT1:79

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₂,b₁ st b₅ is_continuous_on b₃ & b₄ c= b₃ holds
b₅ is_continuous_on b₄

proof end;

theorem Th80: :: NCFCONT1:80

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₄ in dom b₃ holds
b₃ is_continuous_on {b₄}

proof end;

theorem Th81: :: NCFCONT1:81

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Point of b₁ st b₄ in dom b₃ holds
b₃ is_continuous_on {b₄}

proof end;

theorem Th82: :: NCFCONT1:82

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Point of b₂ st b₄ in dom b₃ holds
b₃ is_continuous_on {b₄}

proof end;

theorem Th83: :: NCFCONT1:83

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄, b₅ being PartFunc of b₁,b₂ st b₄ is_continuous_on b₃ & b₅ is_continuous_on b₃ holds
( b₄ + b₅ is_continuous_on b₃ & b₄ - b₅ is_continuous_on b₃ )

proof end;

theorem Th84: :: NCFCONT1:84

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄, b₅ being PartFunc of b₁,b₂ st b₄ is_continuous_on b₃ & b₅ is_continuous_on b₃ holds
( b₄ + b₅ is_continuous_on b₃ & b₄ - b₅ is_continuous_on b₃ )

proof end;

theorem Th85: :: NCFCONT1:85

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄, b₅ being PartFunc of b₂,b₁ st b₄ is_continuous_on b₃ & b₅ is_continuous_on b₃ holds
( b₄ + b₅ is_continuous_on b₃ & b₄ - b₅ is_continuous_on b₃ )

proof end;

theorem Th86: :: NCFCONT1:86

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_continuous_on b₃ & b₆ is_continuous_on b₄ holds
( b₅ + b₆ is_continuous_on b₃ /\ b₄ & b₅ - b₆ is_continuous_on b₃ /\ b₄ )

proof end;

theorem Th87: :: NCFCONT1:87

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_continuous_on b₃ & b₆ is_continuous_on b₄ holds
( b₅ + b₆ is_continuous_on b₃ /\ b₄ & b₅ - b₆ is_continuous_on b₃ /\ b₄ )

proof end;

theorem Th88: :: NCFCONT1:88

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₂,b₁ st b₅ is_continuous_on b₃ & b₆ is_continuous_on b₄ holds
( b₅ + b₆ is_continuous_on b₃ /\ b₄ & b₅ - b₆ is_continuous_on b₃ /\ b₄ )

proof end;

theorem Th89: :: NCFCONT1:89

for b₁ being Complex
for b₂, b₃ being ComplexNormSpace
for b₄ being set
for b₅ being PartFunc of b₂,b₃ st b₅ is_continuous_on b₄ holds
b₁ (#) b₅ is_continuous_on b₄

proof end;

theorem Th90: :: NCFCONT1:90

for b₁ being Real
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being set
for b₅ being PartFunc of b₂,b₃ st b₅ is_continuous_on b₄ holds
b₁ (#) b₅ is_continuous_on b₄

proof end;

theorem Th91: :: NCFCONT1:91

for b₁ being Complex
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being set
for b₅ being PartFunc of b₃,b₂ st b₅ is_continuous_on b₄ holds
b₁ (#) b₅ is_continuous_on b₄

proof end;

theorem Th92: :: NCFCONT1:92

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_continuous_on b₃ holds
( ||.b₄.|| is_continuous_on b₃ & - b₄ is_continuous_on b₃ )

proof end;

theorem Th93: :: NCFCONT1:93

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_continuous_on b₃ holds
( ||.b₄.|| is_continuous_on b₃ & - b₄ is_continuous_on b₃ )

proof end;

theorem Th94: :: NCFCONT1:94

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ st b₄ is_continuous_on b₃ holds
( ||.b₄.|| is_continuous_on b₃ & - b₄ is_continuous_on b₃ )

proof end;

theorem Th95: :: NCFCONT1:95

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂ st b₃ is total & ( for b₄, b₅ being Point of b₁ holds b₃ /. (b₄ + b₅) = (b₃ /. b₄) + (b₃ /. b₅) ) & ex b₄ being Point of b₁ st b₃ is_continuous_in b₄ holds
b₃ is_continuous_on the carrier of b₁

proof end;

theorem Th96: :: NCFCONT1:96

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂ st b₃ is total & ( for b₄, b₅ being Point of b₁ holds b₃ /. (b₄ + b₅) = (b₃ /. b₄) + (b₃ /. b₅) ) & ex b₄ being Point of b₁ st b₃ is_continuous_in b₄ holds
b₃ is_continuous_on the carrier of b₁

proof end;

theorem Th97: :: NCFCONT1:97

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st b₃ is total & ( for b₄, b₅ being Point of b₂ holds b₃ /. (b₄ + b₅) = (b₃ /. b₄) + (b₃ /. b₅) ) & ex b₄ being Point of b₂ st b₃ is_continuous_in b₄ holds
b₃ is_continuous_on the carrier of b₂

proof end;

theorem Th98: :: NCFCONT1:98

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂ st dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
rng b₃ is compact

proof end;

theorem Th99: :: NCFCONT1:99

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂ st dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
rng b₃ is compact

proof end;

theorem Th100: :: NCFCONT1:100

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
rng b₃ is compact

proof end;

theorem Th101: :: NCFCONT1:101

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX st dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
rng b₂ is compact

proof end;

theorem Th102: :: NCFCONT1:102

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
rng b₂ is compact

proof end;

theorem Th103: :: NCFCONT1:103

for b₁ being RealNormSpace
for b₂ being PartFunc of the carrier of b₁, COMPLEX st dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
rng b₂ is compact

proof end;

theorem Th104: :: NCFCONT1:104

for b₁, b₂ being ComplexNormSpace
for b₃ being Subset of b₁
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₃ is compact & b₄ is_continuous_on b₃ holds
b₄ .: b₃ is compact

proof end;

theorem Th105: :: NCFCONT1:105

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being Subset of b₁
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₃ is compact & b₄ is_continuous_on b₃ holds
b₄ .: b₃ is compact

proof end;

theorem Th106: :: NCFCONT1:106

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being Subset of b₂
for b₄ being PartFunc of b₂,b₁ st b₃ c= dom b₄ & b₃ is compact & b₄ is_continuous_on b₃ holds
b₄ .: b₃ is compact

proof end;

theorem Th107: :: NCFCONT1:107

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st dom b₂ <> {} & dom b₂ is compact & b₂ is_continuous_on dom b₂ holds
ex b₃, b₄ being Point of b₁ st
( b₃ in dom b₂ & b₄ in dom b₂ & b₂ /. b₃ = upper_bound (rng b₂) & b₂ /. b₄ = lower_bound (rng b₂) )

proof end;

theorem Th108: :: NCFCONT1:108

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂ st dom b₃ <> {} & dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
ex b₄, b₅ being Point of b₁ st
( b₄ in dom b₃ & b₅ in dom b₃ & ||.b₃.|| /. b₄ = upper_bound (rng ||.b₃.||) & ||.b₃.|| /. b₅ = lower_bound (rng ||.b₃.||) )

proof end;

theorem Th109: :: NCFCONT1:109

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂ st dom b₃ <> {} & dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
ex b₄, b₅ being Point of b₁ st
( b₄ in dom b₃ & b₅ in dom b₃ & ||.b₃.|| /. b₄ = upper_bound (rng ||.b₃.||) & ||.b₃.|| /. b₅ = lower_bound (rng ||.b₃.||) )

proof end;

theorem Th110: :: NCFCONT1:110

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st dom b₃ <> {} & dom b₃ is compact & b₃ is_continuous_on dom b₃ holds
ex b₄, b₅ being Point of b₂ st
( b₄ in dom b₃ & b₅ in dom b₃ & ||.b₃.|| /. b₄ = upper_bound (rng ||.b₃.||) & ||.b₃.|| /. b₅ = lower_bound (rng ||.b₃.||) )

proof end;

theorem Th111: :: NCFCONT1:111

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds ||.b₄.|| | b₃ = ||.(b₄ | b₃).||

proof end;

theorem Th112: :: NCFCONT1:112

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ holds ||.b₄.|| | b₃ = ||.(b₄ | b₃).||

proof end;

theorem Th113: :: NCFCONT1:113

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ holds ||.b₄.|| | b₃ = ||.(b₄ | b₃).||

proof end;

theorem Th114: :: NCFCONT1:114

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Subset of b₁ st b₄ <> {} & b₄ c= dom b₃ & b₄ is compact & b₃ is_continuous_on b₄ holds
ex b₅, b₆ being Point of b₁ st
( b₅ in b₄ & b₆ in b₄ & ||.b₃.|| /. b₅ = upper_bound (||.b₃.|| .: b₄) & ||.b₃.|| /. b₆ = lower_bound (||.b₃.|| .: b₄) )

proof end;

theorem Th115: :: NCFCONT1:115

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂
for b₄ being Subset of b₁ st b₄ <> {} & b₄ c= dom b₃ & b₄ is compact & b₃ is_continuous_on b₄ holds
ex b₅, b₆ being Point of b₁ st
( b₅ in b₄ & b₆ in b₄ & ||.b₃.|| /. b₅ = upper_bound (||.b₃.|| .: b₄) & ||.b₃.|| /. b₆ = lower_bound (||.b₃.|| .: b₄) )

proof end;

theorem Th116: :: NCFCONT1:116

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁
for b₄ being Subset of b₂ st b₄ <> {} & b₄ c= dom b₃ & b₄ is compact & b₃ is_continuous_on b₄ holds
ex b₅, b₆ being Point of b₂ st
( b₅ in b₄ & b₆ in b₄ & ||.b₃.|| /. b₅ = upper_bound (||.b₃.|| .: b₄) & ||.b₃.|| /. b₆ = lower_bound (||.b₃.|| .: b₄) )

proof end;

theorem Th117: :: NCFCONT1:117

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL
for b₃ being Subset of b₁ st b₃ <> {} & b₃ c= dom b₂ & b₃ is compact & b₂ is_continuous_on b₃ holds
ex b₄, b₅ being Point of b₁ st
( b₄ in b₃ & b₅ in b₃ & b₂ /. b₄ = upper_bound (b₂ .: b₃) & b₂ /. b₅ = lower_bound (b₂ .: b₃) )

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be set ;
let c₄ be PartFunc of c₁,c₂;
pred c₄ is_Lipschitzian_on c₃ means :Def27: :: NCFCONT1:def 27
( a₃ c= dom a₄ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₃ & b₃ in a₃ holds
||.((a₄ /. b₂) - (a₄ /. b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def27 defines is_Lipschitzian_on NCFCONT1:def 27 :

definition

let c₁ be ComplexNormSpace;
let c₂ be RealNormSpace;
let c₃ be set ;
let c₄ be PartFunc of c₁,c₂;
pred c₄ is_Lipschitzian_on c₃ means :Def28: :: NCFCONT1:def 28
( a₃ c= dom a₄ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₃ & b₃ in a₃ holds
||.((a₄ /. b₂) - (a₄ /. b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def28 defines is_Lipschitzian_on NCFCONT1:def 28 :

definition

let c₁ be RealNormSpace;
let c₂ be ComplexNormSpace;
let c₃ be set ;
let c₄ be PartFunc of c₁,c₂;
pred c₄ is_Lipschitzian_on c₃ means :Def29: :: NCFCONT1:def 29
( a₃ c= dom a₄ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₃ & b₃ in a₃ holds
||.((a₄ /. b₂) - (a₄ /. b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def29 defines is_Lipschitzian_on NCFCONT1:def 29 :

definition

let c₁ be ComplexNormSpace;
let c₂ be set ;
let c₃ be PartFunc of the carrier of c₁, COMPLEX ;
pred c₃ is_Lipschitzian_on c₂ means :Def30: :: NCFCONT1:def 30
( a₂ c= dom a₃ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
|.((a₃ /. b₂) - (a₃ /. b₃)).| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def30 defines is_Lipschitzian_on NCFCONT1:def 30 :

definition

let c₁ be ComplexNormSpace;
let c₂ be set ;
let c₃ be PartFunc of the carrier of c₁, REAL ;
pred c₃ is_Lipschitzian_on c₂ means :Def31: :: NCFCONT1:def 31
( a₂ c= dom a₃ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
abs ((a₃ /. b₂) - (a₃ /. b₃)) <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def31 defines is_Lipschitzian_on NCFCONT1:def 31 :

definition

let c₁ be RealNormSpace;
let c₂ be set ;
let c₃ be PartFunc of the carrier of c₁, COMPLEX ;
pred c₃ is_Lipschitzian_on c₂ means :Def32: :: NCFCONT1:def 32
( a₂ c= dom a₃ & ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
|.((a₃ /. b₂) - (a₃ /. b₃)).| <= b₁ * ||.(b₂ - b₃).|| ) ) );

end;

:: deftheorem Def32 defines is_Lipschitzian_on NCFCONT1:def 32 :

theorem Th118: :: NCFCONT1:118

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₄ c= b₃ holds
b₅ is_Lipschitzian_on b₄

proof end;

theorem Th119: :: NCFCONT1:119

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₄ c= b₃ holds
b₅ is_Lipschitzian_on b₄

proof end;

theorem Th120: :: NCFCONT1:120

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅ being PartFunc of b₂,b₁ st b₅ is_Lipschitzian_on b₃ & b₄ c= b₃ holds
b₅ is_Lipschitzian_on b₄

proof end;

theorem Th121: :: NCFCONT1:121

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ + b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th122: :: NCFCONT1:122

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ + b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th123: :: NCFCONT1:123

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₂,b₁ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ + b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th124: :: NCFCONT1:124

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ - b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th125: :: NCFCONT1:125

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₁,b₂ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ - b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th126: :: NCFCONT1:126

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃, b₄ being set
for b₅, b₆ being PartFunc of b₂,b₁ st b₅ is_Lipschitzian_on b₃ & b₆ is_Lipschitzian_on b₄ holds
b₅ - b₆ is_Lipschitzian_on b₃ /\ b₄

proof end;

theorem Th127: :: NCFCONT1:127

for b₁ being Complex
for b₂, b₃ being ComplexNormSpace
for b₄ being set
for b₅ being PartFunc of b₂,b₃ st b₅ is_Lipschitzian_on b₄ holds
b₁ (#) b₅ is_Lipschitzian_on b₄

proof end;

theorem Th128: :: NCFCONT1:128

for b₁ being Real
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being set
for b₅ being PartFunc of b₂,b₃ st b₅ is_Lipschitzian_on b₄ holds
b₁ (#) b₅ is_Lipschitzian_on b₄

proof end;

theorem Th129: :: NCFCONT1:129

for b₁ being Complex
for b₂ being ComplexNormSpace
for b₃ being RealNormSpace
for b₄ being set
for b₅ being PartFunc of b₃,b₂ st b₅ is_Lipschitzian_on b₄ holds
b₁ (#) b₅ is_Lipschitzian_on b₄

proof end;

theorem Th130: :: NCFCONT1:130

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_Lipschitzian_on b₃ holds
( - b₄ is_Lipschitzian_on b₃ & ||.b₄.|| is_Lipschitzian_on b₃ )

proof end;

theorem Th131: :: NCFCONT1:131

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_Lipschitzian_on b₃ holds
( - b₄ is_Lipschitzian_on b₃ & ||.b₄.|| is_Lipschitzian_on b₃ )

proof end;

theorem Th132: :: NCFCONT1:132

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ st b₄ is_Lipschitzian_on b₃ holds
( - b₄ is_Lipschitzian_on b₃ & ||.b₄.|| is_Lipschitzian_on b₃ )

proof end;

theorem Th133: :: NCFCONT1:133

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_Lipschitzian_on b₃

proof end;

theorem Th134: :: NCFCONT1:134

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_Lipschitzian_on b₃

proof end;

theorem Th135: :: NCFCONT1:135

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_Lipschitzian_on b₃

proof end;

theorem Th136: :: NCFCONT1:136

for b₁ being ComplexNormSpace
for b₂ being Subset of b₁ holds id b₂ is_Lipschitzian_on b₂

proof end;

theorem Th137: :: NCFCONT1:137

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_Lipschitzian_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th138: :: NCFCONT1:138

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₄ is_Lipschitzian_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th139: :: NCFCONT1:139

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ st b₄ is_Lipschitzian_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th140: :: NCFCONT1:140

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX st b₃ is_Lipschitzian_on b₂ holds
b₃ is_continuous_on b₂

proof end;

theorem Th141: :: NCFCONT1:141

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, REAL st b₃ is_Lipschitzian_on b₂ holds
b₃ is_continuous_on b₂

proof end;

theorem Th142: :: NCFCONT1:142

for b₁ being RealNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, COMPLEX st b₃ is_Lipschitzian_on b₂ holds
b₃ is_continuous_on b₂

proof end;

theorem Th143: :: NCFCONT1:143

for b₁, b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,b₂ st ex b₄ being Point of b₂ st rng b₃ = {b₄} holds
b₃ is_continuous_on dom b₃

proof end;

theorem Th144: :: NCFCONT1:144

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₁,b₂ st ex b₄ being Point of b₂ st rng b₃ = {b₄} holds
b₃ is_continuous_on dom b₃

proof end;

theorem Th145: :: NCFCONT1:145

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being PartFunc of b₂,b₁ st ex b₄ being Point of b₁ st rng b₃ = {b₄} holds
b₃ is_continuous_on dom b₃

proof end;

theorem Th146: :: NCFCONT1:146

for b₁, b₂ being ComplexNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th147: :: NCFCONT1:147

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th148: :: NCFCONT1:148

for b₁ being ComplexNormSpace
for b₂ being RealNormSpace
for b₃ being set
for b₄ being PartFunc of b₂,b₁ st b₃ c= dom b₄ & b₄ is_constant_on b₃ holds
b₄ is_continuous_on b₃

proof end;

theorem Th149: :: NCFCONT1:149

for b₁ being ComplexNormSpace
for b₂ being PartFunc of b₁,b₁ st ( for b₃ being Point of b₁ st b₃ in dom b₂ holds
b₂ /. b₃ = b₃ ) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th150: :: NCFCONT1:150

for b₁ being ComplexNormSpace
for b₂ being PartFunc of b₁,b₁ st b₂ = id (dom b₂) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th151: :: NCFCONT1:151

for b₁ being ComplexNormSpace
for b₂ being PartFunc of b₁,b₁
for b₃ being Subset of b₁ st b₃ c= dom b₂ & b₂ | b₃ = id b₃ holds
b₂ is_continuous_on b₃

proof end;

theorem Th152: :: NCFCONT1:152

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of b₁,b₁
for b₄ being Complex
for b₅ being Point of b₁ st b₂ c= dom b₃ & ( for b₆ being Point of b₁ st b₆ in b₂ holds
b₃ /. b₆ = (b₄ * b₆) + b₅ ) holds
b₃ is_continuous_on b₂

proof end;

theorem Th153: :: NCFCONT1:153

for b₁ being ComplexNormSpace
for b₂ being PartFunc of the carrier of b₁, REAL st ( for b₃ being Point of b₁ st b₃ in dom b₂ holds
b₂ /. b₃ = ||.b₃.|| ) holds
b₂ is_continuous_on dom b₂

proof end;

theorem Th154: :: NCFCONT1:154

for b₁ being ComplexNormSpace
for b₂ being set
for b₃ being PartFunc of the carrier of b₁, REAL st b₂ c= dom b₃ & ( for b₄ being Point of b₁ st b₄ in b₂ holds
b₃ /. b₄ = ||.b₄.|| ) holds
b₃ is_continuous_on b₂

proof end;