:: RFUNCT_1 semantic presentation

Lemma1: (- 1) " = - 1
;

definition

let c₁, c₂ be real-yielding Function;
canceled;
canceled;
canceled;
func c₁ / c₂ -> Function means :Def4: :: RFUNCT_1:def 4
( dom a₃ = (dom a₁) /\ ((dom a₂) \ (a₂ " {0})) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) * ((a₂ . b₁) " ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 RFUNCT_1:def 1 :

:: deftheorem Def2 RFUNCT_1:def 2 :

:: deftheorem Def3 RFUNCT_1:def 3 :

:: deftheorem Def4 defines / RFUNCT_1:def 4 :

registration

let c₁, c₂ be real-yielding Function;
cluster a₁ / a₂ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃, c₄ be PartFunc of c₁,c₂;
redefine func / as c₃ / c₄ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

definition

let c₁ be real-yielding Function;
canceled;
canceled;
canceled;
func c₁ ^ -> Function means :Def8: :: RFUNCT_1:def 8
( dom a₂ = (dom a₁) \ (a₁ " {0}) & ( for b₁ being set st b₁ in dom a₂ holds
a₂ . b₁ = (a₁ . b₁) " ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 RFUNCT_1:def 5 :

:: deftheorem Def6 RFUNCT_1:def 6 :

:: deftheorem Def7 RFUNCT_1:def 7 :

:: deftheorem Def8 defines ^ RFUNCT_1:def 8 :

registration

let c₁ be real-yielding Function;
cluster a₁ ^ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
redefine func ^ as c₃ ^ -> PartFunc of a₁, REAL ;
coherence

proof end;

end;

theorem Th1: :: RFUNCT_1:1

canceled;

theorem Th2: :: RFUNCT_1:2

canceled;

theorem Th3: :: RFUNCT_1:3

canceled;

theorem Th4: :: RFUNCT_1:4

canceled;

theorem Th5: :: RFUNCT_1:5

canceled;

theorem Th6: :: RFUNCT_1:6

canceled;

theorem Th7: :: RFUNCT_1:7

canceled;

theorem Th8: :: RFUNCT_1:8

canceled;

theorem Th9: :: RFUNCT_1:9

canceled;

theorem Th10: :: RFUNCT_1:10

canceled;

theorem Th11: :: RFUNCT_1:11

for b₁ being real-yielding Function holds
( dom (b₁ ^ ) c= dom b₁ & (dom b₁) /\ ((dom b₁) \ (b₁ " {0})) = (dom b₁) \ (b₁ " {0}) )

proof end;

theorem Th12: :: RFUNCT_1:12

for b₁, b₂ being real-yielding Function holds (dom (b₁ (#) b₂)) \ ((b₁ (#) b₂) " {0}) = ((dom b₁) \ (b₁ " {0})) /\ ((dom b₂) \ (b₂ " {0}))

proof end;

theorem Th13: :: RFUNCT_1:13

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being real-yielding Function st b₂ in dom (b₃ ^ ) holds
b₃ . b₂ <> 0

proof end;

theorem Th14: :: RFUNCT_1:14

for b₁ being real-yielding Function holds (b₁ ^ ) " {0} = {}

proof end;

theorem Th15: :: RFUNCT_1:15

for b₁ being real-yielding Function holds
( (abs b₁) " {0} = b₁ " {0} & (- b₁) " {0} = b₁ " {0} )

proof end;

theorem Th16: :: RFUNCT_1:16

for b₁ being real-yielding Function holds dom ((b₁ ^ ) ^ ) = dom (b₁ | (dom (b₁ ^ )))

proof end;

theorem Th17: :: RFUNCT_1:17

for b₁ being real-yielding Function
for b₂ being real number st b₂ <> 0 holds
(b₂ (#) b₁) " {0} = b₁ " {0}

proof end;

theorem Th18: :: RFUNCT_1:18

canceled;

theorem Th19: :: RFUNCT_1:19

for b₁, b₂, b₃ being real-yielding Function holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th20: :: RFUNCT_1:20

canceled;

theorem Th21: :: RFUNCT_1:21

for b₁, b₂, b₃ being real-yielding Function holds (b₁ (#) b₂) (#) b₃ = b₁ (#) (b₂ (#) b₃)

proof end;

theorem Th22: :: RFUNCT_1:22

for b₁, b₂, b₃ being real-yielding Function holds (b₁ + b₂) (#) b₃ = (b₁ (#) b₃) + (b₂ (#) b₃)

proof end;

theorem Th23: :: RFUNCT_1:23

for b₁, b₂, b₃ being real-yielding Function holds b₁ (#) (b₂ + b₃) = (b₁ (#) b₂) + (b₁ (#) b₃) by Th22;

theorem Th24: :: RFUNCT_1:24

for b₁, b₂ being real-yielding Function
for b₃ being real number holds b₃ (#) (b₁ (#) b₂) = (b₃ (#) b₁) (#) b₂

proof end;

theorem Th25: :: RFUNCT_1:25

for b₁, b₂ being real-yielding Function
for b₃ being real number holds b₃ (#) (b₁ (#) b₂) = b₁ (#) (b₃ (#) b₂)

proof end;

theorem Th26: :: RFUNCT_1:26

for b₁, b₂, b₃ being real-yielding Function holds (b₁ - b₂) (#) b₃ = (b₁ (#) b₃) - (b₂ (#) b₃)

proof end;

theorem Th27: :: RFUNCT_1:27

for b₁, b₂, b₃ being real-yielding Function holds (b₁ (#) b₂) - (b₁ (#) b₃) = b₁ (#) (b₂ - b₃) by Th26;

theorem Th28: :: RFUNCT_1:28

for b₁, b₂ being real-yielding Function
for b₃ being real number holds b₃ (#) (b₁ + b₂) = (b₃ (#) b₁) + (b₃ (#) b₂)

proof end;

theorem Th29: :: RFUNCT_1:29

for b₁ being real-yielding Function
for b₂, b₃ being real number holds (b₂ * b₃) (#) b₁ = b₂ (#) (b₃ (#) b₁)

proof end;

theorem Th30: :: RFUNCT_1:30

for b₁, b₂ being real-yielding Function
for b₃ being real number holds b₃ (#) (b₁ - b₂) = (b₃ (#) b₁) - (b₃ (#) b₂)

proof end;

theorem Th31: :: RFUNCT_1:31

for b₁, b₂ being real-yielding Function holds b₁ - b₂ = (- 1) (#) (b₂ - b₁)

proof end;

theorem Th32: :: RFUNCT_1:32

for b₁, b₂, b₃ being real-yielding Function holds b₁ - (b₂ + b₃) = (b₁ - b₂) - b₃

proof end;

theorem Th33: :: RFUNCT_1:33

for b₁ being real-yielding Function holds 1 (#) b₁ = b₁

proof end;

theorem Th34: :: RFUNCT_1:34

for b₁, b₂, b₃ being real-yielding Function holds b₁ - (b₂ - b₃) = (b₁ - b₂) + b₃

proof end;

theorem Th35: :: RFUNCT_1:35

for b₁, b₂, b₃ being real-yielding Function holds b₁ + (b₂ - b₃) = (b₁ + b₂) - b₃

proof end;

theorem Th36: :: RFUNCT_1:36

for b₁, b₂ being real-yielding Function holds abs (b₁ (#) b₂) = (abs b₁) (#) (abs b₂)

proof end;

theorem Th37: :: RFUNCT_1:37

for b₁ being real-yielding Function
for b₂ being real number holds abs (b₂ (#) b₁) = (abs b₂) (#) (abs b₁)

proof end;

theorem Th38: :: RFUNCT_1:38

for b₁ being real-yielding Function holds - b₁ = (- 1) (#) b₁

proof end;

theorem Th39: :: RFUNCT_1:39

for b₁ being real-yielding Function holds - (- b₁) = b₁

proof end;

theorem Th40: :: RFUNCT_1:40

for b₁, b₂ being real-yielding Function holds b₁ - b₂ = b₁ + (- b₂)

proof end;

theorem Th41: :: RFUNCT_1:41

for b₁, b₂ being real-yielding Function holds b₁ - (- b₂) = b₁ + b₂

proof end;

theorem Th42: :: RFUNCT_1:42

for b₁ being real-yielding Function holds (b₁ ^ ) ^ = b₁ | (dom (b₁ ^ ))

proof end;

theorem Th43: :: RFUNCT_1:43

for b₁, b₂ being real-yielding Function holds (b₁ (#) b₂) ^ = (b₁ ^ ) (#) (b₂ ^ )

proof end;

theorem Th44: :: RFUNCT_1:44

for b₁ being real-yielding Function
for b₂ being real number st b₂ <> 0 holds
(b₂ (#) b₁) ^ = (b₂ " ) (#) (b₁ ^ )

proof end;

theorem Th45: :: RFUNCT_1:45

for b₁ being real-yielding Function holds (- b₁) ^ = (- 1) (#) (b₁ ^ )

proof end;

theorem Th46: :: RFUNCT_1:46

for b₁ being real-yielding Function holds (abs b₁) ^ = abs (b₁ ^ )

proof end;

theorem Th47: :: RFUNCT_1:47

for b₁, b₂ being real-yielding Function holds b₁ / b₂ = b₁ (#) (b₂ ^ )

proof end;

theorem Th48: :: RFUNCT_1:48

for b₁, b₂ being real-yielding Function
for b₃ being real number holds b₃ (#) (b₁ / b₂) = (b₃ (#) b₁) / b₂

proof end;

theorem Th49: :: RFUNCT_1:49

for b₁, b₂ being real-yielding Function holds (b₁ / b₂) (#) b₂ = b₁ | (dom (b₂ ^ ))

proof end;

theorem Th50: :: RFUNCT_1:50

for b₁, b₂, b₃, b₄ being real-yielding Function holds (b₁ / b₂) (#) (b₃ / b₄) = (b₁ (#) b₃) / (b₂ (#) b₄)

proof end;

theorem Th51: :: RFUNCT_1:51

for b₁, b₂ being real-yielding Function holds (b₁ / b₂) ^ = (b₂ | (dom (b₂ ^ ))) / b₁

proof end;

theorem Th52: :: RFUNCT_1:52

for b₁, b₂, b₃ being real-yielding Function holds b₁ (#) (b₂ / b₃) = (b₁ (#) b₂) / b₃

proof end;

theorem Th53: :: RFUNCT_1:53

for b₁, b₂, b₃ being real-yielding Function holds b₁ / (b₂ / b₃) = (b₁ (#) (b₃ | (dom (b₃ ^ )))) / b₂

proof end;

theorem Th54: :: RFUNCT_1:54

for b₁, b₂ being real-yielding Function holds
( - (b₁ / b₂) = (- b₁) / b₂ & b₁ / (- b₂) = - (b₁ / b₂) )

proof end;

theorem Th55: :: RFUNCT_1:55

for b₁, b₂, b₃ being real-yielding Function holds
( (b₁ / b₂) + (b₃ / b₂) = (b₁ + b₃) / b₂ & (b₁ / b₂) - (b₃ / b₂) = (b₁ - b₃) / b₂ )

proof end;

theorem Th56: :: RFUNCT_1:56

for b₁, b₂, b₃, b₄ being real-yielding Function holds (b₁ / b₂) + (b₃ / b₄) = ((b₁ (#) b₄) + (b₃ (#) b₂)) / (b₂ (#) b₄)

proof end;

theorem Th57: :: RFUNCT_1:57

for b₁, b₂, b₃, b₄ being real-yielding Function holds (b₁ / b₂) / (b₃ / b₄) = (b₁ (#) (b₄ | (dom (b₄ ^ )))) / (b₂ (#) b₃)

proof end;

theorem Th58: :: RFUNCT_1:58

for b₁, b₂, b₃, b₄ being real-yielding Function holds (b₁ / b₂) - (b₃ / b₄) = ((b₁ (#) b₄) - (b₃ (#) b₂)) / (b₂ (#) b₄)

proof end;

theorem Th59: :: RFUNCT_1:59

for b₁, b₂ being real-yielding Function holds abs (b₁ / b₂) = (abs b₁) / (abs b₂)

proof end;

theorem Th60: :: RFUNCT_1:60

for b₁ being set
for b₂, b₃ being real-yielding Function holds
( (b₂ + b₃) | b₁ = (b₂ | b₁) + (b₃ | b₁) & (b₂ + b₃) | b₁ = (b₂ | b₁) + b₃ & (b₂ + b₃) | b₁ = b₂ + (b₃ | b₁) )

proof end;

theorem Th61: :: RFUNCT_1:61

for b₁ being set
for b₂, b₃ being real-yielding Function holds
( (b₂ (#) b₃) | b₁ = (b₂ | b₁) (#) (b₃ | b₁) & (b₂ (#) b₃) | b₁ = (b₂ | b₁) (#) b₃ & (b₂ (#) b₃) | b₁ = b₂ (#) (b₃ | b₁) )

proof end;

theorem Th62: :: RFUNCT_1:62

for b₁ being set
for b₂ being real-yielding Function holds
( (- b₂) | b₁ = - (b₂ | b₁) & (b₂ ^ ) | b₁ = (b₂ | b₁) ^ & (abs b₂) | b₁ = abs (b₂ | b₁) )

proof end;

theorem Th63: :: RFUNCT_1:63

for b₁ being set
for b₂, b₃ being real-yielding Function holds
( (b₂ - b₃) | b₁ = (b₂ | b₁) - (b₃ | b₁) & (b₂ - b₃) | b₁ = (b₂ | b₁) - b₃ & (b₂ - b₃) | b₁ = b₂ - (b₃ | b₁) )

proof end;

theorem Th64: :: RFUNCT_1:64

for b₁ being set
for b₂, b₃ being real-yielding Function holds
( (b₂ / b₃) | b₁ = (b₂ | b₁) / (b₃ | b₁) & (b₂ / b₃) | b₁ = (b₂ | b₁) / b₃ & (b₂ / b₃) | b₁ = b₂ / (b₃ | b₁) )

proof end;

theorem Th65: :: RFUNCT_1:65

for b₁ being set
for b₂ being real-yielding Function
for b₃ being real number holds (b₃ (#) b₂) | b₁ = b₃ (#) (b₂ | b₁)

proof end;

theorem Th66: :: RFUNCT_1:66

for b₁ being non empty set
for b₂, b₃ being PartFunc of b₁, REAL 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 Th67: :: RFUNCT_1:67

for b₁ being non empty set
for b₂ being real number
for b₃ being PartFunc of b₁, REAL holds
( b₃ is total iff b₂ (#) b₃ is total )

proof end;

theorem Th68: :: RFUNCT_1:68

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

proof end;

theorem Th69: :: RFUNCT_1:69

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

proof end;

theorem Th70: :: RFUNCT_1:70

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

proof end;

theorem Th71: :: RFUNCT_1:71

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

proof end;

theorem Th72: :: RFUNCT_1:72

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being PartFunc of b₁, REAL 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 Th73: :: RFUNCT_1:73

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

proof end;

theorem Th74: :: RFUNCT_1:74

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

proof end;

theorem Th75: :: RFUNCT_1:75

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

proof end;

theorem Th76: :: RFUNCT_1:76

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

proof end;

definition

let c₁, c₂ be set ;
redefine func chi as chi c₁,c₂ -> PartFunc of a₂, REAL ;
coherence

proof end;

end;

theorem Th77: :: RFUNCT_1:77

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, REAL holds
( b₃ = chi b₁,b₂ iff ( dom b₃ = b₂ & ( for b₄ being Element of b₂ holds
( ( b₄ in b₁ implies b₃ . b₄ = 1 ) & ( not b₄ in b₁ implies b₃ . b₄ = 0 ) ) ) ) )

proof end;

theorem Th78: :: RFUNCT_1:78

for b₁ being set
for b₂ being non empty set holds chi b₁,b₂ is total

proof end;

theorem Th79: :: RFUNCT_1:79

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂ holds
( b₃ in b₁ iff (chi b₁,b₂) . b₃ = 1 ) by Th77;

theorem Th80: :: RFUNCT_1:80

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂ holds
( not b₃ in b₁ iff (chi b₁,b₂) . b₃ = 0 ) by Th77;

theorem Th81: :: RFUNCT_1:81

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂ holds
( b₃ in b₂ \ b₁ iff (chi b₁,b₂) . b₃ = 0 )

proof end;

theorem Th82: :: RFUNCT_1:82

canceled;

theorem Th83: :: RFUNCT_1:83

for b₁ being non empty set
for b₂ being Element of b₁ holds (chi b₁,b₁) . b₂ = 1 by Th77;

theorem Th84: :: RFUNCT_1:84

for b₁ being set
for b₂ being non empty set
for b₃ being Element of b₂ holds
( (chi b₁,b₂) . b₃ <> 1 iff (chi b₁,b₂) . b₃ = 0 )

proof end;

theorem Th85: :: RFUNCT_1:85

for b₁, b₂ being set
for b₃ being non empty set st b₁ misses b₂ holds
(chi b₁,b₃) + (chi b₂,b₃) = chi (b₁ \/ b₂),b₃

proof end;

theorem Th86: :: RFUNCT_1:86

for b₁, b₂ being set
for b₃ being non empty set holds (chi b₁,b₃) (#) (chi b₂,b₃) = chi (b₁ /\ b₂),b₃

proof end;

definition

let c₁ be real-yielding Function;
let c₂ be set ;
pred c₁ is_bounded_above_on c₂ means :Def9: :: RFUNCT_1:def 9
ex b₁ being real number st
for b₂ being set st b₂ in a₂ /\ (dom a₁) holds
a₁ . b₂ <= b₁;
pred c₁ is_bounded_below_on c₂ means :Def10: :: RFUNCT_1:def 10
ex b₁ being real number st
for b₂ being set st b₂ in a₂ /\ (dom a₁) holds
b₁ <= a₁ . b₂;

end;

:: deftheorem Def9 defines is_bounded_above_on RFUNCT_1:def 9 :

:: deftheorem Def10 defines is_bounded_below_on RFUNCT_1:def 10 :

definition

let c₁ be real-yielding Function;
let c₂ be set ;
pred c₁ is_bounded_on c₂ means :Def11: :: RFUNCT_1:def 11
( a₁ is_bounded_above_on a₂ & a₁ is_bounded_below_on a₂ );

end;

:: deftheorem Def11 defines is_bounded_on RFUNCT_1:def 11 :

theorem Th87: :: RFUNCT_1:87

canceled;

theorem Th88: :: RFUNCT_1:88

canceled;

theorem Th89: :: RFUNCT_1:89

canceled;

theorem Th90: :: RFUNCT_1:90

for b₁ being set
for b₂ being real-yielding Function holds
( b₂ is_bounded_on b₁ iff ex b₃ being real number st
for b₄ being set st b₄ in b₁ /\ (dom b₂) holds
abs (b₂ . b₄) <= b₃ )

proof end;

theorem Th91: :: RFUNCT_1:91

for b₁, b₂ being set
for b₃ being real-yielding Function holds
( ( b₁ c= b₂ & b₃ is_bounded_above_on b₂ implies b₃ is_bounded_above_on b₁ ) & ( b₁ c= b₂ & b₃ is_bounded_below_on b₂ implies b₃ is_bounded_below_on b₁ ) & ( b₁ c= b₂ & b₃ is_bounded_on b₂ implies b₃ is_bounded_on b₁ ) )

proof end;

theorem Th92: :: RFUNCT_1:92

for b₁, b₂ being set
for b₃ being real-yielding Function st b₃ is_bounded_above_on b₁ & b₃ is_bounded_below_on b₂ holds
b₃ is_bounded_on b₁ /\ b₂

proof end;

theorem Th93: :: RFUNCT_1:93

for b₁ being set
for b₂ being real-yielding Function st b₁ misses dom b₂ holds
b₂ is_bounded_on b₁

proof end;

theorem Th94: :: RFUNCT_1:94

for b₁ being set
for b₂ being real number
for b₃ being real-yielding Function st 0 = b₂ holds
b₂ (#) b₃ is_bounded_on b₁

proof end;

theorem Th95: :: RFUNCT_1:95

for b₁ being set
for b₂ being real number
for b₃ being real-yielding Function holds
( ( b₃ is_bounded_above_on b₁ & 0 <= b₂ implies b₂ (#) b₃ is_bounded_above_on b₁ ) & ( b₃ is_bounded_above_on b₁ & b₂ <= 0 implies b₂ (#) b₃ is_bounded_below_on b₁ ) )

proof end;

theorem Th96: :: RFUNCT_1:96

for b₁ being set
for b₂ being real number
for b₃ being real-yielding Function holds
( ( b₃ is_bounded_below_on b₁ & 0 <= b₂ implies b₂ (#) b₃ is_bounded_below_on b₁ ) & ( b₃ is_bounded_below_on b₁ & b₂ <= 0 implies b₂ (#) b₃ is_bounded_above_on b₁ ) )

proof end;

theorem Th97: :: RFUNCT_1:97

for b₁ being set
for b₂ being real number
for b₃ being real-yielding Function st b₃ is_bounded_on b₁ holds
b₂ (#) b₃ is_bounded_on b₁

proof end;

theorem Th98: :: RFUNCT_1:98

for b₁ being set
for b₂ being real-yielding Function holds abs b₂ is_bounded_below_on b₁

proof end;

theorem Th99: :: RFUNCT_1:99

for b₁ being set
for b₂ being real-yielding Function st b₂ is_bounded_on b₁ holds
( abs b₂ is_bounded_on b₁ & - b₂ is_bounded_on b₁ )

proof end;

theorem Th100: :: RFUNCT_1:100

for b₁, b₂ being set
for b₃, b₄ being real-yielding Function holds
( ( b₃ is_bounded_above_on b₁ & b₄ is_bounded_above_on b₂ implies b₃ + b₄ is_bounded_above_on b₁ /\ b₂ ) & ( b₃ is_bounded_below_on b₁ & b₄ is_bounded_below_on b₂ implies b₃ + b₄ is_bounded_below_on b₁ /\ b₂ ) & ( b₃ is_bounded_on b₁ & b₄ is_bounded_on b₂ implies b₃ + b₄ is_bounded_on b₁ /\ b₂ ) )

proof end;

theorem Th101: :: RFUNCT_1:101

for b₁, b₂ being set
for b₃, b₄ being real-yielding Function 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 Th102: :: RFUNCT_1:102

for b₁, b₂ being set
for b₃ being real-yielding Function st b₃ is_bounded_above_on b₁ & b₃ is_bounded_above_on b₂ holds
b₃ is_bounded_above_on b₁ \/ b₂

proof end;

theorem Th103: :: RFUNCT_1:103

for b₁, b₂ being set
for b₃ being real-yielding Function st b₃ is_bounded_below_on b₁ & b₃ is_bounded_below_on b₂ holds
b₃ is_bounded_below_on b₁ \/ b₂

proof end;

theorem Th104: :: RFUNCT_1:104

for b₁, b₂ being set
for b₃ being real-yielding Function st b₃ is_bounded_on b₁ & b₃ is_bounded_on b₂ holds
b₃ is_bounded_on b₁ \/ b₂

proof end;

theorem Th105: :: RFUNCT_1:105

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, REAL 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 Th106: :: RFUNCT_1:106

for b₁ being set
for b₂ being non empty set
for b₃ being real number
for b₄ being PartFunc of b₂, REAL st b₄ is_constant_on b₁ holds
b₃ (#) b₄ is_constant_on b₁

proof end;

theorem Th107: :: RFUNCT_1:107

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, REAL st b₃ is_constant_on b₁ holds
( abs b₃ is_constant_on b₁ & - b₃ is_constant_on b₁ )

proof end;

theorem Th108: :: RFUNCT_1:108

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

proof end;

theorem Th109: :: RFUNCT_1:109

for b₁ being set
for b₂ being non empty set
for b₃ being PartFunc of b₂, REAL st b₃ is_constant_on b₁ holds
( ( for b₄ being real number holds b₄ (#) b₃ is_bounded_on b₁ ) & - b₃ is_bounded_on b₁ & abs b₃ is_bounded_on b₁ )

proof end;

theorem Th110: :: RFUNCT_1:110

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being PartFunc of b₃, REAL holds
( ( b₄ is_bounded_above_on b₁ & b₅ is_constant_on b₂ implies b₄ + b₅ is_bounded_above_on b₁ /\ b₂ ) & ( b₄ is_bounded_below_on b₁ & b₅ is_constant_on b₂ implies b₄ + b₅ is_bounded_below_on b₁ /\ b₂ ) & ( b₄ is_bounded_on b₁ & b₅ is_constant_on b₂ implies b₄ + b₅ is_bounded_on b₁ /\ b₂ ) )

proof end;

theorem Th111: :: RFUNCT_1:111

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

proof end;