:: CFCONT_1 semantic presentation

definition

let c₁ be PartFunc of COMPLEX , COMPLEX ;
let c₂ be Complex_Sequence;
assume E1: rng c₂ c= dom c₁ ;
func c₁ * c₂ -> Complex_Sequence equals :Def1: :: CFCONT_1:def 1
a₁ * a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines * CFCONT_1:def 1 :

definition

let c₁ be PartFunc of COMPLEX , COMPLEX ;
let c₂ be Element of COMPLEX ;
pred c₁ is_continuous_in c₂ means :Def2: :: CFCONT_1:def 2
( a₂ in dom a₁ & ( for b₁ being Complex_Sequence st rng b₁ c= dom a₁ & b₁ is convergent & lim b₁ = a₂ holds
( a₁ * b₁ is convergent & a₁ /. a₂ = lim (a₁ * b₁) ) ) );

end;

:: deftheorem Def2 defines is_continuous_in CFCONT_1:def 2 :

theorem Th1: :: CFCONT_1:1

canceled;

theorem Th2: :: CFCONT_1:2

for b₁, b₂, b₃ being Complex_Sequence holds
( b₁ = b₂ - b₃ iff for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) - (b₃ . b₄) )

proof end;

theorem Th3: :: CFCONT_1:3

for b₁ being Nat
for b₂ being Complex_Sequence holds rng (b₂ ^\ b₁) c= rng b₂

proof end;

theorem Th4: :: CFCONT_1:4

for b₁ being Nat
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom b₃ holds
b₂ . b₁ in dom b₃

proof end;

theorem Th5: :: CFCONT_1:5

for b₁ being set
for b₂ being Complex_Sequence holds
( b₁ in rng b₂ iff ex b₃ being Nat st b₁ = b₂ . b₃ )

proof end;

theorem Th6: :: CFCONT_1:6

for b₁ being Nat
for b₂ being Complex_Sequence holds b₂ . b₁ in rng b₂ by Th5;

theorem Th7: :: CFCONT_1:7

for b₁, b₂ being Complex_Sequence st b₁ is subsequence of b₂ holds
rng b₁ c= rng b₂

proof end;

theorem Th8: :: CFCONT_1:8

for b₁, b₂ being Complex_Sequence st b₁ is subsequence of b₂ & b₂ is non-zero holds
b₁ is non-zero

proof end;

theorem Th9: :: CFCONT_1:9

for b₁, b₂ being Complex_Sequence
for b₃ being increasing Seq_of_Nat holds
( (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) & (b₁ - b₂) * b₃ = (b₁ * b₃) - (b₂ * b₃) & (b₁ (#) b₂) * b₃ = (b₁ * b₃) (#) (b₂ * b₃) )

proof end;

theorem Th10: :: CFCONT_1:10

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence
for b₃ being increasing Seq_of_Nat holds (b₁ (#) b₂) * b₃ = b₁ (#) (b₂ * b₃)

proof end;

theorem Th11: :: CFCONT_1:11

for b₁ being Complex_Sequence
for b₂ being increasing Seq_of_Nat holds
( (- b₁) * b₂ = - (b₁ * b₂) & |.b₁.| * b₂ = |.(b₁ * b₂).| )

proof end;

theorem Th12: :: CFCONT_1:12

for b₁ being Complex_Sequence
for b₂ being increasing Seq_of_Nat holds (b₁ * b₂) " = (b₁ " ) * b₂

proof end;

theorem Th13: :: CFCONT_1:13

for b₁, b₂ being Complex_Sequence
for b₃ being increasing Seq_of_Nat holds (b₁ /" b₂) * b₃ = (b₁ * b₃) /" (b₂ * b₃)

proof end;

theorem Th14: :: CFCONT_1:14

for b₁ being Complex_Sequence
for b₂ being Subset of COMPLEX st ( for b₃ being Nat holds b₁ . b₃ in b₂ ) holds
rng b₁ c= b₂

proof end;

theorem Th15: :: CFCONT_1:15

canceled;

theorem Th16: :: CFCONT_1:16

for b₁ being Nat
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom b₃ holds
(b₃ * b₂) . b₁ = b₃ /. (b₂ . b₁)

proof end;

theorem Th17: :: CFCONT_1:17

for b₁ being Nat
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom b₃ holds
(b₃ * b₂) ^\ b₁ = b₃ * (b₂ ^\ b₁)

proof end;

theorem Th18: :: CFCONT_1:18

for b₁ being Complex_Sequence
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st rng b₁ c= (dom b₂) /\ (dom b₃) holds
( (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) & (b₂ - b₃) * b₁ = (b₂ * b₁) - (b₃ * b₁) & (b₂ (#) b₃) * b₁ = (b₂ * b₁) (#) (b₃ * b₁) )

proof end;

theorem Th19: :: CFCONT_1:19

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom b₃ holds
(b₁ (#) b₃) * b₂ = b₁ (#) (b₃ * b₂)

proof end;

theorem Th20: :: CFCONT_1:20

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX st rng b₁ c= dom b₂ holds
- (b₂ * b₁) = (- b₂) * b₁

proof end;

theorem Th21: :: CFCONT_1:21

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX st rng b₁ c= dom (b₂ ^ ) holds
b₂ * b₁ is non-zero

proof end;

theorem Th22: :: CFCONT_1:22

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX st rng b₁ c= dom (b₂ ^ ) holds
(b₂ ^ ) * b₁ = (b₂ * b₁) "

proof end;

theorem Th23: :: CFCONT_1:23

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX
for b₃ being increasing Seq_of_Nat st rng b₁ c= dom b₂ holds
Re ((b₂ * b₁) * b₃) = Re (b₂ * (b₁ * b₃))

proof end;

theorem Th24: :: CFCONT_1:24

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX
for b₃ being increasing Seq_of_Nat st rng b₁ c= dom b₂ holds
Im ((b₂ * b₁) * b₃) = Im (b₂ * (b₁ * b₃))

proof end;

theorem Th25: :: CFCONT_1:25

for b₁ being Complex_Sequence
for b₂ being PartFunc of COMPLEX , COMPLEX
for b₃ being increasing Seq_of_Nat st rng b₁ c= dom b₂ holds
(b₂ * b₁) * b₃ = b₂ * (b₁ * b₃)

proof end;

theorem Th26: :: CFCONT_1:26

for b₁, b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₁ c= dom b₃ & b₂ is subsequence of b₁ holds
b₃ * b₂ is subsequence of b₃ * b₁

proof end;

theorem Th27: :: CFCONT_1:27

for b₁ being Nat
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st b₃ is total holds
(b₃ * b₂) . b₁ = b₃ /. (b₂ . b₁)

proof end;

theorem Th28: :: CFCONT_1:28

for b₁ being Nat
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st b₃ is total holds
b₃ * (b₂ ^\ b₁) = (b₃ * b₂) ^\ b₁

proof end;

theorem Th29: :: CFCONT_1:29

for b₁ being Complex_Sequence
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st b₂ is total & b₃ is total holds
( (b₂ + b₃) * b₁ = (b₂ * b₁) + (b₃ * b₁) & (b₂ - b₃) * b₁ = (b₂ * b₁) - (b₃ * b₁) & (b₂ (#) b₃) * b₁ = (b₂ * b₁) (#) (b₃ * b₁) )

proof end;

theorem Th30: :: CFCONT_1:30

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st b₃ is total holds
(b₁ (#) b₃) * b₂ = b₁ (#) (b₃ * b₂)

proof end;

theorem Th31: :: CFCONT_1:31

for b₁ being set
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom (b₃ | b₁) holds
(b₃ | b₁) * b₂ = b₃ * b₂

proof end;

theorem Th32: :: CFCONT_1:32

for b₁ being set
for b₂ being Complex_Sequence
for b₃ being Subset of COMPLEX
for b₄ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom (b₄ | b₁) & ( rng b₂ c= dom (b₄ | b₃) or b₁ c= b₃ ) holds
(b₄ | b₁) * b₂ = (b₄ | b₃) * b₂

proof end;

theorem Th33: :: CFCONT_1:33

for b₁ being set
for b₂ being Complex_Sequence
for b₃ being PartFunc of COMPLEX , COMPLEX st rng b₂ c= dom (b₃ | b₁) & b₃ " {0} = {} holds
((b₃ ^ ) | b₁) * b₂ = ((b₃ | b₁) * b₂) "

proof end;

definition

let c₁ be Complex_Sequence;
canceled;
redefine attr a₁ is constant means :Def4: :: CFCONT_1:def 4
ex b₁ being Element of COMPLEX st
for b₂ being Nat holds a₁ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def3 CFCONT_1:def 3 :

:: deftheorem Def4 defines constant CFCONT_1:def 4 :

Lemma22: for b₁ being Complex_Sequence holds
( ( ex b₂ being Element of COMPLEX st
for b₃ being Nat holds b₁ . b₃ = b₂ implies ex b₂ being Element of COMPLEX st rng b₁ = {b₂} ) & ( ex b₂ being Element of COMPLEX st rng b₁ = {b₂} implies for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) ) & ( ( for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) ) implies for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) ) implies for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ ) implies ex b₂ being Element of COMPLEX st
for b₃ being Nat holds b₁ . b₃ = b₂ ) )

proof end;

theorem Th34: :: CFCONT_1:34

for b₁ being Complex_Sequence holds
( b₁ is constant iff ex b₂ being Element of COMPLEX st rng b₁ = {b₂} )

proof end;

theorem Th35: :: CFCONT_1:35

for b₁ being Complex_Sequence holds
( b₁ is constant iff for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) )

proof end;

theorem Th36: :: CFCONT_1:36

for b₁ being Complex_Sequence holds
( b₁ is constant iff for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) )

proof end;

theorem Th37: :: CFCONT_1:37

for b₁ being Complex_Sequence holds
( b₁ is constant iff for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ )

proof end;

theorem Th38: :: CFCONT_1:38

for b₁ being Nat
for b₂ being Complex_Sequence holds b₂ ^\ b₁ is subsequence of b₂

proof end;

theorem Th39: :: CFCONT_1:39

for b₁, b₂ being Complex_Sequence st b₁ is subsequence of b₂ & b₂ is convergent holds
b₁ is convergent

proof end;

theorem Th40: :: CFCONT_1:40

for b₁, b₂ being Complex_Sequence st b₁ is subsequence of b₂ & b₂ is convergent holds
lim b₁ = lim b₂

proof end;

theorem Th41: :: CFCONT_1:41

for b₁, b₂ being Complex_Sequence st b₁ is convergent & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ = b₁ . b₄ holds
b₂ is convergent

proof end;

theorem Th42: :: CFCONT_1:42

for b₁, b₂ being Complex_Sequence st b₁ is convergent & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ = b₁ . b₄ holds
lim b₁ = lim b₂

proof end;

theorem Th43: :: CFCONT_1:43

for b₁ being Nat
for b₂ being Complex_Sequence st b₂ is convergent holds
( b₂ ^\ b₁ is convergent & lim (b₂ ^\ b₁) = lim b₂ )

proof end;

theorem Th44: :: CFCONT_1:44

for b₁, b₂ being Complex_Sequence st b₁ is convergent & ex b₃ being Nat st b₁ = b₂ ^\ b₃ holds
b₂ is convergent

proof end;

theorem Th45: :: CFCONT_1:45

for b₁, b₂ being Complex_Sequence st b₁ is convergent & ex b₃ being Nat st b₁ = b₂ ^\ b₃ holds
lim b₂ = lim b₁

proof end;

theorem Th46: :: CFCONT_1:46

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0 holds
ex b₂ being Nat st b₁ ^\ b₂ is non-zero

proof end;

theorem Th47: :: CFCONT_1:47

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0 holds
ex b₂ being Complex_Sequence st
( b₂ is subsequence of b₁ & b₂ is non-zero )

proof end;

theorem Th48: :: CFCONT_1:48

for b₁ being Complex_Sequence st b₁ is constant holds
b₁ is convergent

proof end;

theorem Th49: :: CFCONT_1:49

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence st ( ( b₂ is constant & b₁ in rng b₂ ) or ( b₂ is constant & ex b₃ being Nat st b₂ . b₃ = b₁ ) ) holds
lim b₂ = b₁

proof end;

theorem Th50: :: CFCONT_1:50

for b₁ being Complex_Sequence st b₁ is constant holds
for b₂ being Nat holds lim b₁ = b₁ . b₂ by Th49;

theorem Th51: :: CFCONT_1:51

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0 holds
for b₂ being Complex_Sequence st b₂ is subsequence of b₁ & b₂ is non-zero holds
lim (b₂ " ) = (lim b₁) "

proof end;

theorem Th52: :: CFCONT_1:52

for b₁, b₂ being Complex_Sequence st b₁ is constant & b₂ is convergent holds
( lim (b₁ + b₂) = (b₁ . 0) + (lim b₂) & lim (b₁ - b₂) = (b₁ . 0) - (lim b₂) & lim (b₂ - b₁) = (lim b₂) - (b₁ . 0) & lim (b₁ (#) b₂) = (b₁ . 0) * (lim b₂) )

proof end;

scheme :: CFCONT_1:sch 1
s1{ P₁[ set , set ] } :

ex b₁ being Complex_Sequence st
for b₂ being Nat holds P₁[b₂,b₁ . b₂]

provided

E35: for b₁ being Nat ex b₂ being Element of COMPLEX st P₁[b₁,b₂]

proof end;

theorem Th53: :: CFCONT_1:53

for b₁ being Element of COMPLEX
for b₂ being PartFunc of COMPLEX , COMPLEX holds
( b₂ is_continuous_in b₁ iff ( b₁ in dom b₂ & ( for b₃ being Complex_Sequence st rng b₃ c= dom b₂ & b₃ is convergent & lim b₃ = b₁ & ( for b₄ being Nat holds b₃ . b₄ <> b₁ ) holds
( b₂ * b₃ is convergent & b₂ /. b₁ = lim (b₂ * b₃) ) ) ) )

proof end;

theorem Th54: :: CFCONT_1:54

for b₁ being Element of COMPLEX
for b₂ being PartFunc of COMPLEX , COMPLEX 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 Element of COMPLEX st b₅ in dom b₂ & |.(b₅ - b₁).| < b₄ holds
|.((b₂ /. b₅) - (b₂ /. b₁)).| < b₃ ) ) ) ) )

proof end;

theorem Th55: :: CFCONT_1:55

for b₁ being Element of COMPLEX
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_in b₁ & b₃ is_continuous_in b₁ holds
( b₂ + b₃ is_continuous_in b₁ & b₂ - b₃ is_continuous_in b₁ & b₂ (#) b₃ is_continuous_in b₁ )

proof end;

theorem Th56: :: CFCONT_1:56

for b₁, b₂ being Element of COMPLEX
for b₃ being PartFunc of COMPLEX , COMPLEX st b₃ is_continuous_in b₁ holds
b₂ (#) b₃ is_continuous_in b₁

proof end;

theorem Th57: :: CFCONT_1:57

for b₁ being Element of COMPLEX
for b₂ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_in b₁ holds
- b₂ is_continuous_in b₁

proof end;

theorem Th58: :: CFCONT_1:58

for b₁ being Element of COMPLEX
for b₂ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_in b₁ & b₂ /. b₁ <> 0 holds
b₂ ^ is_continuous_in b₁

proof end;

theorem Th59: :: CFCONT_1:59

for b₁ being Element of COMPLEX
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_in b₁ & b₂ /. b₁ <> 0 & b₃ is_continuous_in b₁ holds
b₃ / b₂ is_continuous_in b₁

proof end;

definition

let c₁ be PartFunc of COMPLEX , COMPLEX ;
let c₂ be set ;
pred c₁ is_continuous_on c₂ means :Def5: :: CFCONT_1:def 5
( a₂ c= dom a₁ & ( for b₁ being Element of COMPLEX st b₁ in a₂ holds
a₁ | a₂ is_continuous_in b₁ ) );

end;

:: deftheorem Def5 defines is_continuous_on CFCONT_1:def 5 :

theorem Th60: :: CFCONT_1:60

for b₁ being set
for b₂ being PartFunc of COMPLEX , COMPLEX holds
( b₂ is_continuous_on b₁ iff ( b₁ c= dom b₂ & ( for b₃ being Complex_Sequence 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 Th61: :: CFCONT_1:61

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

proof end;

theorem Th62: :: CFCONT_1:62

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

proof end;

theorem Th63: :: CFCONT_1:63

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

proof end;

theorem Th64: :: CFCONT_1:64

for b₁ being Element of COMPLEX
for b₂ being PartFunc of COMPLEX , COMPLEX st b₁ in dom b₂ holds
b₂ is_continuous_on {b₁}

proof end;

theorem Th65: :: CFCONT_1:65

for b₁ being set
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_on b₁ & b₃ is_continuous_on b₁ holds
( b₂ + b₃ is_continuous_on b₁ & b₂ - b₃ is_continuous_on b₁ & b₂ (#) b₃ is_continuous_on b₁ )

proof end;

theorem Th66: :: CFCONT_1:66

for b₁, b₂ being set
for b₃, b₄ being PartFunc of COMPLEX , COMPLEX 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₂ & b₃ (#) b₄ is_continuous_on b₁ /\ b₂ )

proof end;

theorem Th67: :: CFCONT_1:67

for b₁ being Element of COMPLEX
for b₂ being set
for b₃ being PartFunc of COMPLEX , COMPLEX st b₃ is_continuous_on b₂ holds
b₁ (#) b₃ is_continuous_on b₂

proof end;

theorem Th68: :: CFCONT_1:68

for b₁ being set
for b₂ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_on b₁ holds
- b₂ is_continuous_on b₁

proof end;

theorem Th69: :: CFCONT_1:69

for b₁ being set
for b₂ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_on b₁ & b₂ " {0} = {} holds
b₂ ^ is_continuous_on b₁

proof end;

theorem Th70: :: CFCONT_1:70

for b₁ being set
for b₂ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_on b₁ & (b₂ | b₁) " {0} = {} holds
b₂ ^ is_continuous_on b₁

proof end;

theorem Th71: :: CFCONT_1:71

for b₁ being set
for b₂, b₃ being PartFunc of COMPLEX , COMPLEX st b₂ is_continuous_on b₁ & b₂ " {0} = {} & b₃ is_continuous_on b₁ holds
b₃ / b₂ is_continuous_on b₁

proof end;

theorem Th72: :: CFCONT_1:72

for b₁ being PartFunc of COMPLEX , COMPLEX st b₁ is total & ( for b₂, b₃ being Element of COMPLEX holds b₁ /. (b₂ + b₃) = (b₁ /. b₂) + (b₁ /. b₃) ) & ex b₂ being Element of COMPLEX st b₁ is_continuous_in b₂ holds
b₁ is_continuous_on COMPLEX

proof end;

definition

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

end;

:: deftheorem Def6 defines compact CFCONT_1:def 6 :

theorem Th73: :: CFCONT_1:73

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

proof end;

theorem Th74: :: CFCONT_1:74

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

proof end;