:: Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received May 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1: (- 1) " = - 1
;

::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::
definition
let f1, f2 be complex-valued Function;
func f1 / f2 -> Function means :Def1: :: RFUNCT_1:def 1
( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom it holds
it . c = (f1 . c) * ((f2 . c) ") ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * ((f2 . c) ") ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * ((f2 . c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) * ((f2 . c) ") ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines / RFUNCT_1:def 1 :
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 / f2 iff ( dom b3 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) * ((f2 . c) ") ) ) );

registration
let f1, f2 be complex-valued Function;
cluster f1 / f2 -> complex-valued ;
coherence
f1 / f2 is complex-valued
proof end;
end;

registration
let f1, f2 be real-valued Function;
cluster f1 / f2 -> real-valued ;
coherence
f1 / f2 is real-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: /
redefine func f1 / f2 -> PartFunc of C,COMPLEX;
coherence
f1 / f2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: /
redefine func f1 / f2 -> PartFunc of C,REAL;
coherence
f1 / f2 is PartFunc of C,REAL
proof end;
end;

definition
let f be complex-valued Function;
func f ^ -> Function means :Def2: :: RFUNCT_1:def 2
( dom it = (dom f) \ (f " {0}) & ( for c being set st c in dom it holds
it . c = (f . c) " ) );
existence
ex b1 being Function st
( dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) & dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ^ RFUNCT_1:def 2 :
for f being complex-valued Function
for b2 being Function holds
( b2 = f ^ iff ( dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) ) );

registration
let f be complex-valued Function;
cluster f ^ -> complex-valued ;
coherence
f ^ is complex-valued
proof end;
end;

registration
let f be real-valued Function;
cluster f ^ -> real-valued ;
coherence
f ^ is real-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: ^
redefine func f ^ -> PartFunc of C,COMPLEX;
coherence
f ^ is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: ^
redefine func f ^ -> PartFunc of C,REAL;
coherence
f ^ is PartFunc of C,REAL
proof end;
end;

theorem Th1: :: RFUNCT_1:1
for g being complex-valued Function holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
proof end;

theorem Th2: :: RFUNCT_1:2
for f1, f2 being complex-valued Function holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
proof end;

theorem Th3: :: RFUNCT_1:3
for C being non empty set
for c being Element of C
for f being complex-valued Function st c in dom (f ^) holds
f . c <> 0
proof end;

theorem Th4: :: RFUNCT_1:4
for f being complex-valued Function holds (f ^) " {0} = {}
proof end;

theorem Th5: :: RFUNCT_1:5
for f being complex-valued Function holds
( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} )
proof end;

theorem Th6: :: RFUNCT_1:6
for f being complex-valued Function holds dom ((f ^) ^) = dom (f | (dom (f ^)))
proof end;

theorem Th7: :: RFUNCT_1:7
for f being complex-valued Function
for r being complex number st r <> 0 holds
(r (#) f) " {0} = f " {0}
proof end;

::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem :: RFUNCT_1:8
for f1, f2, f3 being complex-valued Function holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof end;

theorem Th9: :: RFUNCT_1:9
for f1, f2, f3 being complex-valued Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof end;

theorem Th10: :: RFUNCT_1:10
for f1, f2, f3 being complex-valued Function holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof end;

theorem :: RFUNCT_1:11
for f3, f1, f2 being complex-valued Function holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th10;

theorem Th12: :: RFUNCT_1:12
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof end;

theorem Th13: :: RFUNCT_1:13
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof end;

theorem Th14: :: RFUNCT_1:14
for f1, f2, f3 being complex-valued Function holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof end;

theorem :: RFUNCT_1:15
for f3, f1, f2 being complex-valued Function holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th14;

theorem :: RFUNCT_1:16
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof end;

theorem :: RFUNCT_1:17
for f being complex-valued Function
for r, p being complex number holds (r * p) (#) f = r (#) (p (#) f)
proof end;

theorem :: RFUNCT_1:18
for f1, f2 being complex-valued Function
for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof end;

theorem :: RFUNCT_1:19
for f1, f2 being complex-valued Function holds f1 - f2 = (- 1) (#) (f2 - f1)
proof end;

theorem :: RFUNCT_1:20
for f1, f2, f3 being complex-valued Function holds f1 - (f2 + f3) = (f1 - f2) - f3
proof end;

theorem :: RFUNCT_1:21
for f being complex-valued Function holds 1 (#) f = f
proof end;

theorem :: RFUNCT_1:22
for f1, f2, f3 being complex-valued Function holds f1 - (f2 - f3) = (f1 - f2) + f3
proof end;

theorem :: RFUNCT_1:23
for f1, f2, f3 being complex-valued Function holds f1 + (f2 - f3) = (f1 + f2) - f3
proof end;

theorem Th24: :: RFUNCT_1:24
for f1, f2 being complex-valued Function holds abs (f1 (#) f2) = (abs f1) (#) (abs f2)
proof end;

theorem :: RFUNCT_1:25
for f being complex-valued Function
for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f)
proof end;

theorem Th26: :: RFUNCT_1:26
for f being complex-valued Function holds (f ^) ^ = f | (dom (f ^))
proof end;

theorem Th27: :: RFUNCT_1:27
for f1, f2 being complex-valued Function holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
proof end;

theorem Th28: :: RFUNCT_1:28
for f being complex-valued Function
for r being complex number st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
proof end;

theorem :: RFUNCT_1:29
for f being complex-valued Function holds (- f) ^ = (- 1) (#) (f ^) by Lm1, Th28;

theorem Th30: :: RFUNCT_1:30
for f being complex-valued Function holds (abs f) ^ = abs (f ^)
proof end;

theorem Th31: :: RFUNCT_1:31
for f, g being complex-valued Function holds f / g = f (#) (g ^)
proof end;

theorem Th32: :: RFUNCT_1:32
for g, f being complex-valued Function
for r being complex number holds r (#) (g / f) = (r (#) g) / f
proof end;

theorem :: RFUNCT_1:33
for f, g being complex-valued Function holds (f / g) (#) g = f | (dom (g ^))
proof end;

theorem Th34: :: RFUNCT_1:34
for f, g, f1, g1 being complex-valued Function holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
proof end;

theorem Th35: :: RFUNCT_1:35
for f1, f2 being complex-valued Function holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
proof end;

theorem Th36: :: RFUNCT_1:36
for g, f1, f2 being complex-valued Function holds g (#) (f1 / f2) = (g (#) f1) / f2
proof end;

theorem :: RFUNCT_1:37
for g, f1, f2 being complex-valued Function holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
proof end;

theorem :: RFUNCT_1:38
for f, g being complex-valued Function holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
proof end;

theorem :: RFUNCT_1:39
for f1, f, f2 being complex-valued Function holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
proof end;

theorem Th40: :: RFUNCT_1:40
for f1, f, g1, g being complex-valued Function holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
proof end;

theorem :: RFUNCT_1:41
for f, g, f1, g1 being complex-valued Function holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
proof end;

theorem :: RFUNCT_1:42
for f1, f, g1, g being complex-valued Function holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
proof end;

theorem :: RFUNCT_1:43
for f1, f2 being complex-valued Function holds abs (f1 / f2) = (abs f1) / (abs f2)
proof end;

theorem Th44: :: RFUNCT_1:44
for X being set
for f1, f2 being complex-valued Function holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof end;

theorem Th45: :: RFUNCT_1:45
for X being set
for f1, f2 being complex-valued Function holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof end;

theorem Th46: :: RFUNCT_1:46
for X being set
for f being complex-valued Function holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) )
proof end;

theorem :: RFUNCT_1:47
for X being set
for f1, f2 being complex-valued Function holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof end;

theorem :: RFUNCT_1:48
for X being set
for f1, f2 being complex-valued Function holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
proof end;

theorem Th49: :: RFUNCT_1:49
for X being set
for f being complex-valued Function
for r being complex number holds (r (#) f) | X = r (#) (f | X)
proof end;

theorem Th50: :: RFUNCT_1:50
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof end;

theorem Th51: :: RFUNCT_1:51
for C being non empty set
for r being real number
for f being PartFunc of C,REAL holds
( f is total iff r (#) f is total )
proof end;

theorem :: RFUNCT_1:52
for C being non empty set
for f being PartFunc of C,REAL holds
( f is total iff - f is total ) by Th51;

theorem :: RFUNCT_1:53
for C being non empty set
for f being PartFunc of C,REAL holds
( f is total iff abs f is total )
proof end;

theorem Th54: :: RFUNCT_1:54
for C being non empty set
for f being PartFunc of C,REAL holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
proof end;

theorem Th55: :: RFUNCT_1:55
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
proof end;

theorem :: RFUNCT_1:56
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds
( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )
proof end;

theorem :: RFUNCT_1:57
for C being non empty set
for c being Element of C
for r being real number
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)
proof end;

theorem :: RFUNCT_1:58
for C being non empty set
for c being Element of C
for f being PartFunc of C,REAL st f is total holds
( (- f) . c = - (f . c) & (abs f) . c = abs (f . c) ) by VALUED_1:8, VALUED_1:18;

theorem :: RFUNCT_1:59
for C being non empty set
for c being Element of C
for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
proof end;

theorem :: RFUNCT_1:60
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds
(f1 / f2) . c = (f1 . c) * ((f2 . c) ")
proof end;

::
:: CHARCTERISTIC FUNCTION OF A SUBSET OF A DOMAIN
::
definition
let X, C be set ;
:: original: chi
redefine func chi (X,C) -> PartFunc of C,REAL;
coherence
chi (X,C) is PartFunc of C,REAL
proof end;
end;

registration
let X, C be set ;
cluster chi (X,C) -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = chi (X,C) holds
b1 is total
proof end;
end;

theorem Th61: :: RFUNCT_1:61
for X being set
for C being non empty set
for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )
proof end;

theorem :: RFUNCT_1:62
for X being set
for C being non empty set holds chi (X,C) is total ;

theorem :: RFUNCT_1:63
for X being set
for C being non empty set
for c being Element of C holds
( c in X iff (chi (X,C)) . c = 1 ) by Th61;

theorem :: RFUNCT_1:64
for X being set
for C being non empty set
for c being Element of C holds
( not c in X iff (chi (X,C)) . c = 0 ) by Th61;

theorem :: RFUNCT_1:65
for X being set
for C being non empty set
for c being Element of C holds
( c in C \ X iff (chi (X,C)) . c = 0 )
proof end;

theorem :: RFUNCT_1:66
for C being non empty set
for c being Element of C holds (chi (C,C)) . c = 1 by Th61;

theorem Th67: :: RFUNCT_1:67
for X being set
for C being non empty set
for c being Element of C holds
( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 )
proof end;

theorem :: RFUNCT_1:68
for X, Y being set
for C being non empty set st X misses Y holds
(chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C)
proof end;

theorem :: RFUNCT_1:69
for X, Y being set
for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
proof end;

theorem Th70: :: RFUNCT_1:70
for Y being set
for f being real-valued Function holds
( f | Y is bounded_above iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r )
proof end;

theorem Th71: :: RFUNCT_1:71
for Y being set
for f being real-valued Function holds
( f | Y is bounded_below iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c )
proof end;

theorem Th72: :: RFUNCT_1:72
for f being real-valued Function holds
( f is bounded iff ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r )
proof end;

theorem :: RFUNCT_1:73
for Y being set
for f being real-valued Function holds
( f | Y is bounded iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )
proof end;

theorem :: RFUNCT_1:74
for Y, X being set
for f being real-valued Function holds
( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) )
proof end;

theorem :: RFUNCT_1:75
for X, Y being set
for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds
f | (X /\ Y) is bounded
proof end;

registration
cluster Relation-like Function-like constant real-valued -> real-valued bounded for set ;
coherence
for b1 being real-valued Function st b1 is constant holds
b1 is bounded
proof end;
end;

theorem :: RFUNCT_1:76
for X being set
for f being real-valued Function st X misses dom f holds
f | X is bounded
proof end;

theorem :: RFUNCT_1:77
for Y being set
for f being real-valued Function holds (0 (#) f) | Y is bounded
proof end;

registration
let f be real-valued bounded_above Function;
let X be set ;
cluster f | X -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_above
proof end;
end;

registration
let f be real-valued bounded_below Function;
let X be set ;
cluster f | X -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f | X holds
b1 is bounded_below
proof end;
end;

registration
let f be real-valued bounded_above Function;
let r be non negative real number ;
cluster r (#) f -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above
proof end;
end;

registration
let f be real-valued bounded_below Function;
let r be non negative real number ;
cluster r (#) f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below
proof end;
end;

registration
let f be real-valued bounded_above Function;
let r be non positive real number ;
cluster r (#) f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_below
proof end;
end;

registration
let f be real-valued bounded_below Function;
let r be non positive real number ;
cluster r (#) f -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = r (#) f holds
b1 is bounded_above
proof end;
end;

theorem Th78: :: RFUNCT_1:78
for Y being set
for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) )
proof end;

theorem Th79: :: RFUNCT_1:79
for Y being set
for r being real number
for f being real-valued Function holds
( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) )
proof end;

theorem Th80: :: RFUNCT_1:80
for Y being set
for r being real number
for f being real-valued Function st f | Y is bounded holds
(r (#) f) | Y is bounded
proof end;

registration
let f be real-valued Function;
cluster |.f.| -> bounded_below ;
coherence
abs f is bounded_below
proof end;
end;

theorem :: RFUNCT_1:81
for X being set
for f being real-valued Function holds (abs f) | X is bounded_below ;

registration
let f be real-valued bounded Function;
cluster |.f.| -> real-valued bounded for real-valued Function;
coherence
for b1 being real-valued Function st b1 = abs f holds
b1 is bounded
proof end;
end;

registration
let f be real-valued bounded_above Function;
cluster - f -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = - f holds
b1 is bounded_below ;
end;

theorem Th82: :: RFUNCT_1:82
for Y being set
for f being real-valued Function st f | Y is bounded holds
( (abs f) | Y is bounded & (- f) | Y is bounded )
proof end;

registration
let f1, f2 be real-valued bounded_above Function;
cluster f1 + f2 -> real-valued bounded_above for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_above
proof end;
end;

registration
let f1, f2 be real-valued bounded_below Function;
cluster f1 + f2 -> real-valued bounded_below for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_below
proof end;
end;

theorem Th83: :: RFUNCT_1:83
for X, Y being set
for f1, f2 being real-valued Function holds
( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
proof end;

registration
let f1, f2 be real-valued bounded Function;
cluster f1 (#) f2 -> real-valued bounded for real-valued Function;
coherence
for b1 being real-valued Function st b1 = f1 (#) f2 holds
b1 is bounded
proof end;
end;

theorem Th84: :: RFUNCT_1:84
for X, Y being set
for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof end;

theorem Th85: :: RFUNCT_1:85
for X, Y being set
for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds
f | (X \/ Y) is bounded_above
proof end;

theorem Th86: :: RFUNCT_1:86
for X, Y being set
for f being real-valued Function st f | X is bounded_below & f | Y is bounded_below holds
f | (X \/ Y) is bounded_below
proof end;

theorem :: RFUNCT_1:87
for X, Y being set
for f being real-valued Function st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
proof end;

registration
let C be non empty set ;
let f1, f2 be constant PartFunc of C,REAL;
cluster f1 + f2 -> constant ;
coherence
f1 + f2 is constant
proof end;
cluster f1 - f2 -> constant ;
coherence
f1 - f2 is constant
proof end;
cluster f1 (#) f2 -> constant ;
coherence
f1 (#) f2 is constant
proof end;
end;

theorem :: RFUNCT_1:88
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
proof end;

registration
let C be non empty set ;
let f be constant PartFunc of C,REAL;
cluster - f -> constant ;
coherence
- f is constant
proof end;
cluster |.f.| -> constant ;
coherence
abs f is constant
proof end;
let p be real number ;
cluster p (#) f -> constant ;
coherence
p (#) f is constant
proof end;
end;

theorem Th89: :: RFUNCT_1:89
for Y being set
for C being non empty set
for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
proof end;

theorem Th90: :: RFUNCT_1:90
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(- f) | Y is constant
proof end;

theorem Th91: :: RFUNCT_1:91
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
(abs f) | Y is constant
proof end;

theorem :: RFUNCT_1:92
for Y being set
for C being non empty set
for f being PartFunc of C,REAL st f | Y is constant holds
( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )
proof end;

theorem :: RFUNCT_1:93
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded ) ) by Th83;

theorem :: RFUNCT_1:94
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) )
proof end;