:: by Jaros{\l}aw Kotowicz

::

:: Received May 27, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: (- 1) " = - 1

;

definition

let f1, f2 be complex-valued Function;

ex b_{1} being Function st

( dom b_{1} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) * ((f2 . c) ") ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) * ((f2 . c) ") ) & dom b_{2} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f1 . c) * ((f2 . c) ") ) holds

b_{1} = b_{2}

end;
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 ( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom it holds

it . c = (f1 . c) * ((f2 . c) ") ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines / RFUNCT_1:def 1 :

for f1, f2 being complex-valued Function

for b_{3} being Function holds

( b_{3} = f1 / f2 iff ( dom b_{3} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b_{3} holds

b_{3} . c = (f1 . c) * ((f2 . c) ") ) ) );

for f1, f2 being complex-valued Function

for b

( b

b

registration
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

end;
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;

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

end;
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;

definition

let f be complex-valued Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) \ (f " {0}) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) " ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) \ (f " {0}) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) " ) & dom b_{2} = (dom f) \ (f " {0}) & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) " ) holds

b_{1} = b_{2}

end;
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 ( dom it = (dom f) \ (f " {0}) & ( for c being set st c in dom it holds

it . c = (f . c) " ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines ^ RFUNCT_1:def 2 :

for f being complex-valued Function

for b_{2} being Function holds

( b_{2} = f ^ iff ( dom b_{2} = (dom f) \ (f " {0}) & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) " ) ) );

for f being complex-valued Function

for b

( b

b

registration
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

end;
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;

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

end;
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;

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}) )

( 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

for c being Element of C

for f being complex-valued Function st c in dom (f ^) holds

f . c <> 0

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}

for r being complex number st r <> 0 holds

(r (#) f) " {0} = f " {0}

proof end;

::

:: BASIC PROPERTIES OF OPERATIONS

::

:: BASIC PROPERTIES OF OPERATIONS

::

theorem :: RFUNCT_1:11

theorem Th12: :: RFUNCT_1:12

for f1, f2 being complex-valued Function

for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

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)

for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

proof end;

theorem :: RFUNCT_1:15

theorem :: RFUNCT_1:16

for f1, f2 being complex-valued Function

for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

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)

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)

for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) 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)

for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f)

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 ^)

for r being complex number st r <> 0 holds

(r (#) f) ^ = (r ") (#) (f ^)

proof end;

theorem :: RFUNCT_1:29

theorem Th32: :: RFUNCT_1:32

for g, f being complex-valued Function

for r being complex number holds r (#) (g / f) = (r (#) g) / f

for r being complex number holds r (#) (g / f) = (r (#) g) / f

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 :: 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 )

( (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 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) )

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) )

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) )

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) )

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) )

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)

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 ) ) )

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 )

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

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 ) )

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 )

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) )

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)

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

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) "

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) ")

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

::

:: 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

end;
:: original: chi

redefine func chi (X,C) -> PartFunc of C,REAL;

coherence

chi (X,C) is PartFunc of C,REAL

proof end;

registration

let X, C be set ;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = chi (X,C) holds

b_{1} is total

end;
coherence

for b

b

proof 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 ) ) ) ) )

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:63

theorem :: RFUNCT_1:64

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 )

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

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 )

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)

for C being non empty set st X misses Y 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 )

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 )

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 )

( 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 )

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 ) )

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

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

coherence

for b_{1} being real-valued Function st b_{1} is constant holds

b_{1} is bounded

end;
for b

b

proof end;

registration

let f be real-valued bounded_above Function;

let X be set ;

coherence

for b_{1} being real-valued Function st b_{1} = f | X holds

b_{1} is bounded_above

end;
let X be set ;

coherence

for b

b

proof end;

registration

let f be real-valued bounded_below Function;

let X be set ;

coherence

for b_{1} being real-valued Function st b_{1} = f | X holds

b_{1} is bounded_below

end;
let X be set ;

coherence

for b

b

proof end;

registration

let f be real-valued bounded_above Function;

let r be non negative real number ;

coherence

for b_{1} being real-valued Function st b_{1} = r (#) f holds

b_{1} is bounded_above

end;
let r be non negative real number ;

coherence

for b

b

proof end;

registration

let f be real-valued bounded_below Function;

let r be non negative real number ;

coherence

for b_{1} being real-valued Function st b_{1} = r (#) f holds

b_{1} is bounded_below

end;
let r be non negative real number ;

coherence

for b

b

proof end;

registration

let f be real-valued bounded_above Function;

let r be non positive real number ;

coherence

for b_{1} being real-valued Function st b_{1} = r (#) f holds

b_{1} is bounded_below

end;
let r be non positive real number ;

coherence

for b

b

proof end;

registration

let f be real-valued bounded_below Function;

let r be non positive real number ;

coherence

for b_{1} being real-valued Function st b_{1} = r (#) f holds

b_{1} is bounded_above

end;
let r be non positive real number ;

coherence

for b

b

proof 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 ) )

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 ) )

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

for r being real number

for f being real-valued Function st f | Y is bounded holds

(r (#) f) | Y is bounded

proof end;

theorem :: RFUNCT_1:81

registration

let f be real-valued bounded Function;

coherence

for b_{1} being real-valued Function st b_{1} = abs f holds

b_{1} is bounded

end;
coherence

for b

b

proof end;

registration

let f be real-valued bounded_above Function;

coherence

for b_{1} being real-valued Function st b_{1} = - f holds

b_{1} is bounded_below
;

end;
coherence

for b

b

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 )

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;

coherence

for b_{1} being real-valued Function st b_{1} = f1 + f2 holds

b_{1} is bounded_above

end;
coherence

for b

b

proof end;

registration

let f1, f2 be real-valued bounded_below Function;

coherence

for b_{1} being real-valued Function st b_{1} = f1 + f2 holds

b_{1} is bounded_below

end;
coherence

for b

b

proof 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 ) )

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;

coherence

for b_{1} being real-valued Function st b_{1} = f1 (#) f2 holds

b_{1} is bounded

end;
coherence

for b

b

proof 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 )

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

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

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

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;

coherence

f1 + f2 is constant

f1 - f2 is constant

f1 (#) f2 is constant

end;
let f1, f2 be constant PartFunc of C,REAL;

coherence

f1 + f2 is constant

proof end;

coherence f1 - f2 is constant

proof end;

coherence f1 (#) f2 is constant

proof 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 )

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;

coherence

- f is constant

abs f is constant

coherence

p (#) f is constant

end;
let f be constant PartFunc of C,REAL;

coherence

- f is constant

proof end;

coherence abs f is constant

proof end;

let p be real number ;coherence

p (#) f is constant

proof 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

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

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

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 )

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;

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 ) ) )

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;

::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS

::