:: CFUNCT_1 semantic presentation

definition

mode Complex is Element of COMPLEX ;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be PartFunc of c₁, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (c₂ /. a₁) * ((c₃ /. a₁) " );
func c₂ / c₃ -> PartFunc of a₁, COMPLEX means :Def1: :: CFUNCT_1:def 1
( dom a₄ = (dom a₂) /\ ((dom a₃) \ (a₃ " {0})) & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ /. b₁ = (a₂ /. b₁) * ((a₃ /. b₁) " ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines / CFUNCT_1:def 1 :

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (c₂ /. a₁) " ;
func c₂ ^ -> PartFunc of a₁, COMPLEX means :Def2: :: CFUNCT_1:def 2
( dom a₃ = (dom a₂) \ (a₂ " {0}) & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ /. b₁ = (a₂ /. b₁) " ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ^ CFUNCT_1:def 2 :

theorem Th1: :: CFUNCT_1:1

canceled;

theorem Th2: :: CFUNCT_1:2

canceled;

theorem Th3: :: CFUNCT_1:3

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( dom (b₂ + b₃) = (dom b₂) /\ (dom b₃) & ( for b₄ being Element of b₁ st b₄ in dom (b₂ + b₃) holds
(b₂ + b₃) /. b₄ = (b₂ /. b₄) + (b₃ /. b₄) ) )

proof end;

theorem Th4: :: CFUNCT_1:4

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( dom (b₂ - b₃) = (dom b₂) /\ (dom b₃) & ( for b₄ being Element of b₁ st b₄ in dom (b₂ - b₃) holds
(b₂ - b₃) /. b₄ = (b₂ /. b₄) - (b₃ /. b₄) ) )

proof end;

theorem Th5: :: CFUNCT_1:5

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( dom (b₂ (#) b₃) = (dom b₂) /\ (dom b₃) & ( for b₄ being Element of b₁ st b₄ in dom (b₂ (#) b₃) holds
(b₂ (#) b₃) /. b₄ = (b₂ /. b₄) * (b₃ /. b₄) ) )

proof end;

theorem Th6: :: CFUNCT_1:6

canceled;

theorem Th7: :: CFUNCT_1:7

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃ being Element of COMPLEX holds
( dom (b₃ (#) b₂) = dom b₂ & ( for b₄ being Element of b₁ st b₄ in dom (b₃ (#) b₂) holds
(b₃ (#) b₂) /. b₄ = b₃ * (b₂ /. b₄) ) )

proof end;

theorem Th8: :: CFUNCT_1:8

canceled;

theorem Th9: :: CFUNCT_1:9

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( dom (- b₂) = dom b₂ & ( for b₃ being Element of b₁ st b₃ in dom (- b₂) holds
(- b₂) /. b₃ = - (b₂ /. b₃) ) )

proof end;

Lemma8: for b₁, b₂ being set
for b₃ being non empty set
for b₄ being PartFunc of b₃, COMPLEX holds
( b₁ in b₄ " b₂ iff ( b₁ in dom b₄ & b₄ /. b₁ in b₂ ) )
by PARTFUN2:44;

theorem Th10: :: CFUNCT_1:10

canceled;

theorem Th11: :: CFUNCT_1:11

canceled;

theorem Th12: :: CFUNCT_1:12

canceled;

theorem Th13: :: CFUNCT_1:13

canceled;

theorem Th14: :: CFUNCT_1:14

canceled;

theorem Th15: :: CFUNCT_1:15

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( dom (b₂ ^ ) c= dom b₂ & (dom b₂) /\ ((dom b₂) \ (b₂ " {0})) = (dom b₂) \ (b₂ " {0}) )

proof end;

theorem Th16: :: CFUNCT_1:16

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds (dom (b₂ (#) b₃)) \ ((b₂ (#) b₃) " {0}) = ((dom b₂) \ (b₂ " {0})) /\ ((dom b₃) \ (b₃ " {0}))

proof end;

theorem Th17: :: CFUNCT_1:17

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being PartFunc of b₁, COMPLEX st b₂ in dom (b₃ ^ ) holds
b₃ /. b₂ <> 0

proof end;

theorem Th18: :: CFUNCT_1:18

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds (b₂ ^ ) " {0} = {}

proof end;

theorem Th19: :: CFUNCT_1:19

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( |.b₂.| " {0} = b₂ " {0} & (- b₂) " {0} = b₂ " {0} )

proof end;

theorem Th20: :: CFUNCT_1:20

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds dom ((b₂ ^ ) ^ ) = dom (b₂ | (dom (b₂ ^ )))

proof end;

theorem Th21: :: CFUNCT_1:21

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃ being Element of COMPLEX st b₃ <> 0 holds
(b₃ (#) b₂) " {0} = b₂ " {0}

proof end;

theorem Th22: :: CFUNCT_1:22

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th23: :: CFUNCT_1:23

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds (b₂ (#) b₃) (#) b₄ = b₂ (#) (b₃ (#) b₄)

proof end;

theorem Th24: :: CFUNCT_1:24

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds (b₂ + b₃) (#) b₄ = (b₂ (#) b₄) + (b₃ (#) b₄)

proof end;

theorem Th25: :: CFUNCT_1:25

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ (#) (b₃ + b₄) = (b₂ (#) b₃) + (b₂ (#) b₄) by Th24;

theorem Th26: :: CFUNCT_1:26

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX holds b₄ (#) (b₂ (#) b₃) = (b₄ (#) b₂) (#) b₃

proof end;

theorem Th27: :: CFUNCT_1:27

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX holds b₄ (#) (b₂ (#) b₃) = b₂ (#) (b₄ (#) b₃)

proof end;

theorem Th28: :: CFUNCT_1:28

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds (b₂ - b₃) (#) b₄ = (b₂ (#) b₄) - (b₃ (#) b₄)

proof end;

theorem Th29: :: CFUNCT_1:29

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds (b₂ (#) b₃) - (b₂ (#) b₄) = b₂ (#) (b₃ - b₄) by Th28;

theorem Th30: :: CFUNCT_1:30

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX holds b₄ (#) (b₂ + b₃) = (b₄ (#) b₂) + (b₄ (#) b₃)

proof end;

theorem Th31: :: CFUNCT_1:31

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃, b₄ being Element of COMPLEX holds (b₃ * b₄) (#) b₂ = b₃ (#) (b₄ (#) b₂)

proof end;

theorem Th32: :: CFUNCT_1:32

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX holds b₄ (#) (b₂ - b₃) = (b₄ (#) b₂) - (b₄ (#) b₃)

proof end;

theorem Th33: :: CFUNCT_1:33

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds b₂ - b₃ = (- 1r ) (#) (b₃ - b₂)

proof end;

theorem Th34: :: CFUNCT_1:34

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ - (b₃ + b₄) = (b₂ - b₃) - b₄

proof end;

theorem Th35: :: CFUNCT_1:35

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds 1r (#) b₂ = b₂

proof end;

theorem Th36: :: CFUNCT_1:36

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th37: :: CFUNCT_1:37

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ + (b₃ - b₄) = (b₂ + b₃) - b₄

proof end;

theorem Th38: :: CFUNCT_1:38

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds |.(b₂ (#) b₃).| = |.b₂.| (#) |.b₃.|

proof end;

theorem Th39: :: CFUNCT_1:39

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃ being Element of COMPLEX holds |.(b₃ (#) b₂).| = |.b₃.| (#) |.b₂.|

proof end;

theorem Th40: :: CFUNCT_1:40

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds - b₂ = (- 1r ) (#) b₂

proof end;

theorem Th41: :: CFUNCT_1:41

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds - (- b₂) = b₂

proof end;

theorem Th42: :: CFUNCT_1:42

canceled;

theorem Th43: :: CFUNCT_1:43

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds b₂ - (- b₃) = b₂ + b₃

proof end;

theorem Th44: :: CFUNCT_1:44

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds (b₂ ^ ) ^ = b₂ | (dom (b₂ ^ ))

proof end;

theorem Th45: :: CFUNCT_1:45

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds (b₂ (#) b₃) ^ = (b₂ ^ ) (#) (b₃ ^ )

proof end;

theorem Th46: :: CFUNCT_1:46

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃ being Element of COMPLEX st b₃ <> 0 holds
(b₃ (#) b₂) ^ = (b₃ " ) (#) (b₂ ^ )

proof end;

Lemma30: (- 1r ) " = - 1r
by COMPLEX1:def 7;

theorem Th47: :: CFUNCT_1:47

canceled;

theorem Th48: :: CFUNCT_1:48

canceled;

theorem Th49: :: CFUNCT_1:49

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds (- b₂) ^ = (- 1r ) (#) (b₂ ^ )

proof end;

theorem Th50: :: CFUNCT_1:50

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds |.b₂.| ^ = |.(b₂ ^ ).|

proof end;

theorem Th51: :: CFUNCT_1:51

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds b₂ / b₃ = b₂ (#) (b₃ ^ )

proof end;

theorem Th52: :: CFUNCT_1:52

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX holds b₄ (#) (b₂ / b₃) = (b₄ (#) b₂) / b₃

proof end;

theorem Th53: :: CFUNCT_1:53

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) (#) b₃ = b₂ | (dom (b₃ ^ ))

proof end;

theorem Th54: :: CFUNCT_1:54

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) (#) (b₄ / b₅) = (b₂ (#) b₄) / (b₃ (#) b₅)

proof end;

theorem Th55: :: CFUNCT_1:55

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) ^ = (b₃ | (dom (b₃ ^ ))) / b₂

proof end;

theorem Th56: :: CFUNCT_1:56

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ (#) (b₃ / b₄) = (b₂ (#) b₃) / b₄

proof end;

theorem Th57: :: CFUNCT_1:57

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds b₂ / (b₃ / b₄) = (b₂ (#) (b₄ | (dom (b₄ ^ )))) / b₃

proof end;

theorem Th58: :: CFUNCT_1:58

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( - (b₂ / b₃) = (- b₂) / b₃ & b₂ / (- b₃) = - (b₂ / b₃) )

proof end;

theorem Th59: :: CFUNCT_1:59

for b₁ being non empty set
for b₂, b₃, b₄ being PartFunc of b₁, COMPLEX holds
( (b₂ / b₃) + (b₄ / b₃) = (b₂ + b₄) / b₃ & (b₂ / b₃) - (b₄ / b₃) = (b₂ - b₄) / b₃ )

proof end;

theorem Th60: :: CFUNCT_1:60

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) + (b₄ / b₅) = ((b₂ (#) b₅) + (b₄ (#) b₃)) / (b₃ (#) b₅)

proof end;

theorem Th61: :: CFUNCT_1:61

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) / (b₄ / b₅) = (b₂ (#) (b₅ | (dom (b₅ ^ )))) / (b₃ (#) b₄)

proof end;

theorem Th62: :: CFUNCT_1:62

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₂ / b₃) - (b₄ / b₅) = ((b₂ (#) b₅) - (b₄ (#) b₃)) / (b₃ (#) b₅)

proof end;

theorem Th63: :: CFUNCT_1:63

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds |.(b₂ / b₃).| = |.b₂.| / |.b₃.|

proof end;

theorem Th64: :: CFUNCT_1:64

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being PartFunc of b₂, COMPLEX holds
( (b₃ + b₄) | b₁ = (b₃ | b₁) + (b₄ | b₁) & (b₃ + b₄) | b₁ = (b₃ | b₁) + b₄ & (b₃ + b₄) | b₁ = b₃ + (b₄ | b₁) )

proof end;

theorem Th65: :: CFUNCT_1:65

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being PartFunc of b₂, COMPLEX holds
( (b₃ (#) b₄) | b₁ = (b₃ | b₁) (#) (b₄ | b₁) & (b₃ (#) b₄) | b₁ = (b₃ | b₁) (#) b₄ & (b₃ (#) b₄) | b₁ = b₃ (#) (b₄ | b₁) )

proof end;

theorem Th66: :: CFUNCT_1:66

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX holds
( (- b₃) | b₁ = - (b₃ | b₁) & (b₃ ^ ) | b₁ = (b₃ | b₁) ^ & |.b₃.| | b₁ = |.(b₃ | b₁).| )

proof end;

theorem Th67: :: CFUNCT_1:67

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being PartFunc of b₂, COMPLEX holds
( (b₃ - b₄) | b₁ = (b₃ | b₁) - (b₄ | b₁) & (b₃ - b₄) | b₁ = (b₃ | b₁) - b₄ & (b₃ - b₄) | b₁ = b₃ - (b₄ | b₁) )

proof end;

theorem Th68: :: CFUNCT_1:68

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being PartFunc of b₂, COMPLEX holds
( (b₃ / b₄) | b₁ = (b₃ | b₁) / (b₄ | b₁) & (b₃ / b₄) | b₁ = (b₃ | b₁) / b₄ & (b₃ / b₄) | b₁ = b₃ / (b₄ | b₁) )

proof end;

theorem Th69: :: CFUNCT_1:69

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX
for b₄ being Element of COMPLEX holds (b₄ (#) b₃) | b₁ = b₄ (#) (b₃ | b₁)

proof end;

theorem Th70: :: CFUNCT_1:70

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( ( b₂ is total & b₃ is total implies b₂ + b₃ is total ) & ( b₂ + b₃ is total implies ( b₂ is total & b₃ is total ) ) & ( b₂ is total & b₃ is total implies b₂ - b₃ is total ) & ( b₂ - b₃ is total implies ( b₂ is total & b₃ is total ) ) & ( b₂ is total & b₃ is total implies b₂ (#) b₃ is total ) & ( b₂ (#) b₃ is total implies ( b₂ is total & b₃ is total ) ) )

proof end;

theorem Th71: :: CFUNCT_1:71

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX
for b₃ being Element of COMPLEX holds
( b₂ is total iff b₃ (#) b₂ is total )

proof end;

theorem Th72: :: CFUNCT_1:72

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( b₂ is total iff - b₂ is total )

proof end;

theorem Th73: :: CFUNCT_1:73

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( b₂ is total iff |.b₂.| is total )

proof end;

theorem Th74: :: CFUNCT_1:74

for b₁ being non empty set
for b₂ being PartFunc of b₁, COMPLEX holds
( b₂ ^ is total iff ( b₂ " {0} = {} & b₂ is total ) )

proof end;

theorem Th75: :: CFUNCT_1:75

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, COMPLEX holds
( ( b₂ is total & b₃ " {0} = {} & b₃ is total ) iff b₂ / b₃ is total )

proof end;

theorem Th76: :: CFUNCT_1:76

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being PartFunc of b₁, 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 Th77: :: CFUNCT_1:77

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being PartFunc of b₁, COMPLEX
for b₄ being Element of COMPLEX st b₃ is total holds
(b₄ (#) b₃) /. b₂ = b₄ * (b₃ /. b₂)

proof end;

theorem Th78: :: CFUNCT_1:78

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being PartFunc of b₁, COMPLEX st b₃ is total holds
( (- b₃) /. b₂ = - (b₃ /. b₂) & |.b₃.| . b₂ = |.(b₃ /. b₂).| )

proof end;

theorem Th79: :: CFUNCT_1:79

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being PartFunc of b₁, COMPLEX st b₃ ^ is total holds
(b₃ ^ ) /. b₂ = (b₃ /. b₂) "

proof end;

theorem Th80: :: CFUNCT_1:80

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being PartFunc of b₁, COMPLEX st b₃ is total & b₄ ^ is total holds
(b₃ / b₄) /. b₂ = (b₃ /. b₂) * ((b₄ /. b₂) " )

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, COMPLEX ;
let c₃ be set ;
pred c₂ is_bounded_on c₃ means :Def3: :: CFUNCT_1:def 3
|.a₂.| is_bounded_on a₃;

end;

:: deftheorem Def3 defines is_bounded_on CFUNCT_1:def 3 :

theorem Th81: :: CFUNCT_1:81

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX holds
( b₃ is_bounded_on b₁ iff ex b₄ being real number st
for b₅ being Element of b₂ st b₅ in b₁ /\ (dom b₃) holds
|.(b₃ /. b₅).| <= b₄ )

proof end;

theorem Th82: :: CFUNCT_1:82

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being PartFunc of b₃, COMPLEX st b₁ c= b₂ & b₄ is_bounded_on b₂ holds
b₄ is_bounded_on b₁

proof end;

theorem Th83: :: CFUNCT_1:83

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX st b₁ misses dom b₃ holds
b₃ is_bounded_on b₁

proof end;

theorem Th84: :: CFUNCT_1:84

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX
for b₄ being Element of COMPLEX st b₃ is_bounded_on b₁ holds
b₄ (#) b₃ is_bounded_on b₁

proof end;

theorem Th85: :: CFUNCT_1:85

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX holds |.b₃.| is_bounded_below_on b₁

proof end;

theorem Th86: :: CFUNCT_1:86

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX st b₃ is_bounded_on b₁ holds
( |.b₃.| is_bounded_on b₁ & - b₃ is_bounded_on b₁ )

proof end;

theorem Th87: :: CFUNCT_1:87

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, COMPLEX st b₄ is_bounded_on b₁ & b₅ is_bounded_on b₂ holds
b₄ + b₅ is_bounded_on b₁ /\ b₂

proof end;

theorem Th88: :: CFUNCT_1:88

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, COMPLEX st b₄ is_bounded_on b₁ & b₅ is_bounded_on b₂ holds
( b₄ (#) b₅ is_bounded_on b₁ /\ b₂ & b₄ - b₅ is_bounded_on b₁ /\ b₂ )

proof end;

theorem Th89: :: CFUNCT_1:89

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being PartFunc of b₃, COMPLEX st b₄ is_bounded_on b₁ & b₄ is_bounded_on b₂ holds
b₄ is_bounded_on b₁ \/ b₂

proof end;

theorem Th90: :: CFUNCT_1:90

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, COMPLEX st b₄ is_constant_on b₁ & b₅ is_constant_on b₂ holds
( b₄ + b₅ is_constant_on b₁ /\ b₂ & b₄ - b₅ is_constant_on b₁ /\ b₂ & b₄ (#) b₅ is_constant_on b₁ /\ b₂ )

proof end;

theorem Th91: :: CFUNCT_1:91

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX
for b₄ being Element of COMPLEX st b₃ is_constant_on b₁ holds
b₄ (#) b₃ is_constant_on b₁

proof end;

theorem Th92: :: CFUNCT_1:92

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX st b₃ is_constant_on b₁ holds
( |.b₃.| is_constant_on b₁ & - b₃ is_constant_on b₁ )

proof end;

theorem Th93: :: CFUNCT_1:93

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX st b₃ is_constant_on b₁ holds
b₃ is_bounded_on b₁

proof end;

theorem Th94: :: CFUNCT_1:94

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, COMPLEX st b₃ is_constant_on b₁ holds
( ( for b₄ being Element of COMPLEX holds b₄ (#) b₃ is_bounded_on b₁ ) & - b₃ is_bounded_on b₁ & |.b₃.| is_bounded_on b₁ )

proof end;

theorem Th95: :: CFUNCT_1:95

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, COMPLEX st b₄ is_bounded_on b₁ & b₅ is_constant_on b₂ holds
b₄ + b₅ is_bounded_on b₁ /\ b₂

proof end;

theorem Th96: :: CFUNCT_1:96

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, COMPLEX st b₄ is_bounded_on b₁ & b₅ is_constant_on b₂ holds
( b₄ - b₅ is_bounded_on b₁ /\ b₂ & b₅ - b₄ is_bounded_on b₁ /\ b₂ & b₄ (#) b₅ is_bounded_on b₁ /\ b₂ )

proof end;