:: RFUNCT_2 semantic presentation

theorem Th1: :: RFUNCT_2:1

canceled;

theorem Th2: :: RFUNCT_2:2

for b₁, b₂ being Function
for b₃ being set holds (b₂ | (b₁ .: b₃)) * (b₁ | b₃) = (b₂ * b₁) | b₃

proof end;

theorem Th3: :: RFUNCT_2:3

for b₁, b₂ being Function
for b₃, b₄ being set holds (b₂ | b₄) * (b₁ | b₃) = (b₂ * b₁) | (b₃ /\ (b₁ " b₄))

proof end;

theorem Th4: :: RFUNCT_2:4

for b₁, b₂ being Function
for b₃ being set holds
( b₃ c= dom (b₂ * b₁) iff ( b₃ c= dom b₁ & b₁ .: b₃ c= dom b₂ ) )

proof end;

theorem Th5: :: RFUNCT_2:5

for b₁ being Function
for b₂ being set holds (b₁ | b₂) .: b₂ = b₁ .: b₂

proof end;

definition

let c₁ be Real_Sequence;
redefine func rng as rng c₁ -> Subset of REAL ;
coherence by RELSET_1:12;

end;

theorem Th6: :: RFUNCT_2:6

for b₁, b₂, b₃ being Real_Sequence holds
( b₁ = b₂ - b₃ iff for b₄ being Element of NAT holds b₁ . b₄ = (b₂ . b₄) - (b₃ . b₄) )

proof end;

theorem Th7: :: RFUNCT_2:7

for b₁ being Real_Sequence
for b₂ being Element of NAT holds rng (b₁ ^\ b₂) c= rng b₁

proof end;

theorem Th8: :: RFUNCT_2:8

for b₁ being Real_Sequence
for b₂ being Element of NAT
for b₃ being PartFunc of REAL , REAL st rng b₁ c= dom b₃ holds
b₁ . b₂ in dom b₃

proof end;

theorem Th9: :: RFUNCT_2:9

for b₁ being set
for b₂ being Real_Sequence holds
( b₁ in rng b₂ iff ex b₃ being Element of NAT st b₁ = b₂ . b₃ )

proof end;

theorem Th10: :: RFUNCT_2:10

for b₁ being Real_Sequence
for b₂ being Element of NAT holds b₁ . b₂ in rng b₁ by Th9;

theorem Th11: :: RFUNCT_2:11

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

proof end;

theorem Th12: :: RFUNCT_2:12

for b₁, b₂ being Real_Sequence st b₁ is subsequence of b₂ & b₂ is_not_0 holds
b₁ is_not_0

proof end;

theorem Th13: :: RFUNCT_2:13

for b₁, b₂ being Real_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 Th14: :: RFUNCT_2:14

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

proof end;

theorem Th15: :: RFUNCT_2:15

for b₁ being Real_Sequence
for b₂ being increasing Seq_of_Nat holds
( (- b₁) * b₂ = - (b₁ * b₂) & (abs b₁) * b₂ = abs (b₁ * b₂) )

proof end;

theorem Th16: :: RFUNCT_2:16

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

proof end;

theorem Th17: :: RFUNCT_2:17

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

proof end;

theorem Th18: :: RFUNCT_2:18

for b₁ being Real_Sequence st b₁ is convergent & ( for b₂ being Element of NAT holds b₁ . b₂ <= 0 ) holds
lim b₁ <= 0

proof end;

theorem Th19: :: RFUNCT_2:19

for b₁ being set
for b₂ being Real_Sequence st ( for b₃ being Element of NAT holds b₂ . b₃ in b₁ ) holds
rng b₂ c= b₁

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Real_Sequence;
assume E10: rng c₂ c= dom c₁ ;
func c₁ * c₂ -> Real_Sequence equals :Def1: :: RFUNCT_2:def 1
a₁ * a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines * RFUNCT_2:def 1 :

theorem Th20: :: RFUNCT_2:20

canceled;

theorem Th21: :: RFUNCT_2:21

for b₁ being Real_Sequence
for b₂ being Element of NAT
for b₃ being PartFunc of REAL , REAL st rng b₁ c= dom b₃ holds
(b₃ * b₁) . b₂ = b₃ . (b₁ . b₂)

proof end;

theorem Th22: :: RFUNCT_2:22

for b₁ being Real_Sequence
for b₂ being Element of NAT
for b₃ being PartFunc of REAL , REAL st rng b₁ c= dom b₃ holds
(b₃ * b₁) ^\ b₂ = b₃ * (b₁ ^\ b₂)

proof end;

theorem Th23: :: RFUNCT_2:23

for b₁ being Real_Sequence
for b₂, b₃ being PartFunc of REAL , REAL 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 Th24: :: RFUNCT_2:24

for b₁ being Real_Sequence
for b₂ being PartFunc of REAL , REAL
for b₃ being real number st rng b₁ c= dom b₂ holds
(b₃ (#) b₂) * b₁ = b₃ (#) (b₂ * b₁)

proof end;

theorem Th25: :: RFUNCT_2:25

for b₁ being Real_Sequence
for b₂ being PartFunc of REAL , REAL st rng b₁ c= dom b₂ holds
( abs (b₂ * b₁) = (abs b₂) * b₁ & - (b₂ * b₁) = (- b₂) * b₁ )

proof end;

theorem Th26: :: RFUNCT_2:26

for b₁ being Real_Sequence
for b₂ being PartFunc of REAL , REAL st rng b₁ c= dom (b₂ ^ ) holds
b₂ * b₁ is_not_0

proof end;

theorem Th27: :: RFUNCT_2:27

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

proof end;

theorem Th28: :: RFUNCT_2:28

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

proof end;

theorem Th29: :: RFUNCT_2:29

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

proof end;

theorem Th30: :: RFUNCT_2:30

for b₁ being Real_Sequence
for b₂ being Element of NAT
for b₃ being PartFunc of REAL , REAL st b₃ is total holds
(b₃ * b₁) . b₂ = b₃ . (b₁ . b₂)

proof end;

theorem Th31: :: RFUNCT_2:31

for b₁ being Real_Sequence
for b₂ being Element of NAT
for b₃ being PartFunc of REAL , REAL st b₃ is total holds
b₃ * (b₁ ^\ b₂) = (b₃ * b₁) ^\ b₂

proof end;

theorem Th32: :: RFUNCT_2:32

for b₁ being Real_Sequence
for b₂, b₃ being PartFunc of REAL , 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 Th33: :: RFUNCT_2:33

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

proof end;

theorem Th34: :: RFUNCT_2:34

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

proof end;

theorem Th35: :: RFUNCT_2:35

for b₁, b₂ being set
for b₃ being Real_Sequence
for b₄ being PartFunc of REAL , REAL 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 Th36: :: RFUNCT_2:36

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

proof end;

theorem Th37: :: RFUNCT_2:37

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

proof end;

theorem Th38: :: RFUNCT_2:38

for b₁ being Real_Sequence
for b₂ being PartFunc of REAL , REAL st rng b₁ c= dom b₂ holds
b₂ .: (rng b₁) = rng (b₂ * b₁)

proof end;

theorem Th39: :: RFUNCT_2:39

for b₁ being Real_Sequence
for b₂, b₃ being PartFunc of REAL , REAL st rng b₁ c= dom (b₂ * b₃) holds
b₂ * (b₃ * b₁) = (b₂ * b₃) * b₁

proof end;

registration

let c₁ be set ;
let c₂ be one-to-one Function;
cluster a₂ | a₁ -> one-to-one ;
coherence by FUNCT_1:84;

end;

theorem Th40: :: RFUNCT_2:40

for b₁ being set
for b₂ being one-to-one Function holds (b₂ | b₁) " = (b₂ " ) | (b₂ .: b₁)

proof end;

theorem Th41: :: RFUNCT_2:41

for b₁ being PartFunc of REAL , REAL st rng b₁ is bounded & upper_bound (rng b₁) = lower_bound (rng b₁) holds
b₁ is_constant_on dom b₁

proof end;

theorem Th42: :: RFUNCT_2:42

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ .: b₁ is bounded & upper_bound (b₂ .: b₁) = lower_bound (b₂ .: b₁) holds
b₂ is_constant_on b₁

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be set ;
pred c₁ is_increasing_on c₂ means :Def2: :: RFUNCT_2:def 2
for b₁, b₂ being Element of REAL st b₁ in a₂ /\ (dom a₁) & b₂ in a₂ /\ (dom a₁) & b₁ < b₂ holds
a₁ . b₁ < a₁ . b₂;
pred c₁ is_decreasing_on c₂ means :Def3: :: RFUNCT_2:def 3
for b₁, b₂ being Element of REAL st b₁ in a₂ /\ (dom a₁) & b₂ in a₂ /\ (dom a₁) & b₁ < b₂ holds
a₁ . b₂ < a₁ . b₁;
pred c₁ is_non_decreasing_on c₂ means :Def4: :: RFUNCT_2:def 4
for b₁, b₂ being Element of REAL st b₁ in a₂ /\ (dom a₁) & b₂ in a₂ /\ (dom a₁) & b₁ < b₂ holds
a₁ . b₁ <= a₁ . b₂;
pred c₁ is_non_increasing_on c₂ means :Def5: :: RFUNCT_2:def 5
for b₁, b₂ being Element of REAL st b₁ in a₂ /\ (dom a₁) & b₂ in a₂ /\ (dom a₁) & b₁ < b₂ holds
a₁ . b₂ <= a₁ . b₁;

end;

:: deftheorem Def2 defines is_increasing_on RFUNCT_2:def 2 :

:: deftheorem Def3 defines is_decreasing_on RFUNCT_2:def 3 :

:: deftheorem Def4 defines is_non_decreasing_on RFUNCT_2:def 4 :

:: deftheorem Def5 defines is_non_increasing_on RFUNCT_2:def 5 :

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be set ;
pred c₁ is_monotone_on c₂ means :Def6: :: RFUNCT_2:def 6
( a₁ is_non_decreasing_on a₂ or a₁ is_non_increasing_on a₂ );

end;

:: deftheorem Def6 defines is_monotone_on RFUNCT_2:def 6 :

theorem Th43: :: RFUNCT_2:43

canceled;

theorem Th44: :: RFUNCT_2:44

canceled;

theorem Th45: :: RFUNCT_2:45

canceled;

theorem Th46: :: RFUNCT_2:46

canceled;

theorem Th47: :: RFUNCT_2:47

canceled;

theorem Th48: :: RFUNCT_2:48

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_non_decreasing_on b₁ iff for b₃, b₄ being Element of REAL st b₃ in b₁ /\ (dom b₂) & b₄ in b₁ /\ (dom b₂) & b₃ <= b₄ holds
b₂ . b₃ <= b₂ . b₄ )

proof end;

theorem Th49: :: RFUNCT_2:49

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_non_increasing_on b₁ iff for b₃, b₄ being Element of REAL st b₃ in b₁ /\ (dom b₂) & b₄ in b₁ /\ (dom b₂) & b₃ <= b₄ holds
b₂ . b₄ <= b₂ . b₃ )

proof end;

theorem Th50: :: RFUNCT_2:50

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_increasing_on b₁ iff b₂ | b₁ is_increasing_on b₁ )

proof end;

theorem Th51: :: RFUNCT_2:51

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_decreasing_on b₁ iff b₂ | b₁ is_decreasing_on b₁ )

proof end;

theorem Th52: :: RFUNCT_2:52

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_non_decreasing_on b₁ iff b₂ | b₁ is_non_decreasing_on b₁ )

proof end;

theorem Th53: :: RFUNCT_2:53

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_non_increasing_on b₁ iff b₂ | b₁ is_non_increasing_on b₁ )

proof end;

theorem Th54: :: RFUNCT_2:54

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ misses dom b₂ holds
( b₂ is_increasing_on b₁ & b₂ is_decreasing_on b₁ & b₂ is_non_decreasing_on b₁ & b₂ is_non_increasing_on b₁ & b₂ is_monotone_on b₁ )

proof end;

theorem Th55: :: RFUNCT_2:55

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_increasing_on b₁ holds
b₂ is_non_decreasing_on b₁

proof end;

theorem Th56: :: RFUNCT_2:56

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_decreasing_on b₁ holds
b₂ is_non_increasing_on b₁

proof end;

theorem Th57: :: RFUNCT_2:57

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_constant_on b₁ holds
b₂ is_non_decreasing_on b₁

proof end;

theorem Th58: :: RFUNCT_2:58

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_constant_on b₁ holds
b₂ is_non_increasing_on b₁

proof end;

theorem Th59: :: RFUNCT_2:59

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₃ is_non_decreasing_on b₁ & b₃ is_non_increasing_on b₂ holds
b₃ is_constant_on b₁ /\ b₂

proof end;

theorem Th60: :: RFUNCT_2:60

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₁ c= b₂ & b₃ is_increasing_on b₂ holds
b₃ is_increasing_on b₁

proof end;

theorem Th61: :: RFUNCT_2:61

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₁ c= b₂ & b₃ is_decreasing_on b₂ holds
b₃ is_decreasing_on b₁

proof end;

theorem Th62: :: RFUNCT_2:62

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₁ c= b₂ & b₃ is_non_decreasing_on b₂ holds
b₃ is_non_decreasing_on b₁

proof end;

theorem Th63: :: RFUNCT_2:63

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₁ c= b₂ & b₃ is_non_increasing_on b₂ holds
b₃ is_non_increasing_on b₁

proof end;

theorem Th64: :: RFUNCT_2:64

for b₁ being set
for b₂ being Element of REAL
for b₃ being PartFunc of REAL , REAL holds
( ( b₃ is_increasing_on b₁ & 0 < b₂ implies b₂ (#) b₃ is_increasing_on b₁ ) & ( b₂ = 0 implies b₂ (#) b₃ is_constant_on b₁ ) & ( b₃ is_increasing_on b₁ & b₂ < 0 implies b₂ (#) b₃ is_decreasing_on b₁ ) )

proof end;

theorem Th65: :: RFUNCT_2:65

for b₁ being set
for b₂ being Element of REAL
for b₃ being PartFunc of REAL , REAL holds
( ( b₃ is_decreasing_on b₁ & 0 < b₂ implies b₂ (#) b₃ is_decreasing_on b₁ ) & ( b₃ is_decreasing_on b₁ & b₂ < 0 implies b₂ (#) b₃ is_increasing_on b₁ ) )

proof end;

theorem Th66: :: RFUNCT_2:66

for b₁ being set
for b₂ being Element of REAL
for b₃ being PartFunc of REAL , REAL holds
( ( b₃ is_non_decreasing_on b₁ & 0 <= b₂ implies b₂ (#) b₃ is_non_decreasing_on b₁ ) & ( b₃ is_non_decreasing_on b₁ & b₂ <= 0 implies b₂ (#) b₃ is_non_increasing_on b₁ ) )

proof end;

theorem Th67: :: RFUNCT_2:67

for b₁ being set
for b₂ being Element of REAL
for b₃ being PartFunc of REAL , REAL holds
( ( b₃ is_non_increasing_on b₁ & 0 <= b₂ implies b₂ (#) b₃ is_non_increasing_on b₁ ) & ( b₃ is_non_increasing_on b₁ & b₂ <= 0 implies b₂ (#) b₃ is_non_decreasing_on b₁ ) )

proof end;

theorem Th68: :: RFUNCT_2:68

for b₁, b₂ being set
for b₃ being Element of REAL
for b₄, b₅ being PartFunc of REAL , REAL st b₃ in (b₁ /\ b₂) /\ (dom (b₄ + b₅)) holds
( b₃ in b₁ /\ (dom b₄) & b₃ in b₂ /\ (dom b₅) )

proof end;

theorem Th69: :: RFUNCT_2:69

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL holds
( ( b₃ is_increasing_on b₁ & b₄ is_increasing_on b₂ implies b₃ + b₄ is_increasing_on b₁ /\ b₂ ) & ( b₃ is_decreasing_on b₁ & b₄ is_decreasing_on b₂ implies b₃ + b₄ is_decreasing_on b₁ /\ b₂ ) & ( b₃ is_non_decreasing_on b₁ & b₄ is_non_decreasing_on b₂ implies b₃ + b₄ is_non_decreasing_on b₁ /\ b₂ ) & ( b₃ is_non_increasing_on b₁ & b₄ is_non_increasing_on b₂ implies b₃ + b₄ is_non_increasing_on b₁ /\ b₂ ) )

proof end;

theorem Th70: :: RFUNCT_2:70

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL holds
( ( b₃ is_increasing_on b₁ & b₄ is_constant_on b₂ implies b₃ + b₄ is_increasing_on b₁ /\ b₂ ) & ( b₃ is_decreasing_on b₁ & b₄ is_constant_on b₂ implies b₃ + b₄ is_decreasing_on b₁ /\ b₂ ) )

proof end;

theorem Th71: :: RFUNCT_2:71

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_increasing_on b₁ & b₄ is_non_decreasing_on b₂ holds
b₃ + b₄ is_increasing_on b₁ /\ b₂

proof end;

theorem Th72: :: RFUNCT_2:72

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_non_increasing_on b₁ & b₄ is_constant_on b₂ holds
b₃ + b₄ is_non_increasing_on b₁ /\ b₂

proof end;

theorem Th73: :: RFUNCT_2:73

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_decreasing_on b₁ & b₄ is_non_increasing_on b₂ holds
b₃ + b₄ is_decreasing_on b₁ /\ b₂

proof end;

theorem Th74: :: RFUNCT_2:74

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_non_decreasing_on b₁ & b₄ is_constant_on b₂ holds
b₃ + b₄ is_non_decreasing_on b₁ /\ b₂

proof end;

theorem Th75: :: RFUNCT_2:75

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds b₂ is_increasing_on {b₁}

proof end;

theorem Th76: :: RFUNCT_2:76

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds b₂ is_decreasing_on {b₁}

proof end;

theorem Th77: :: RFUNCT_2:77

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds b₂ is_non_decreasing_on {b₁}

proof end;

theorem Th78: :: RFUNCT_2:78

for b₁ being set
for b₂ being PartFunc of REAL , REAL holds b₂ is_non_increasing_on {b₁}

proof end;

theorem Th79: :: RFUNCT_2:79

for b₁ being Subset of REAL holds id b₁ is_increasing_on b₁

proof end;

theorem Th80: :: RFUNCT_2:80

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_increasing_on b₁ holds
- b₂ is_decreasing_on b₁

proof end;

theorem Th81: :: RFUNCT_2:81

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_non_decreasing_on b₁ holds
- b₂ is_non_increasing_on b₁

proof end;

theorem Th82: :: RFUNCT_2:82

for b₁, b₂ being Element of REAL
for b₃ being PartFunc of REAL , REAL st ( b₃ is_increasing_on [.b₁,b₂.] or b₃ is_decreasing_on [.b₁,b₂.] ) holds
b₃ | [.b₁,b₂.] is one-to-one

proof end;

theorem Th83: :: RFUNCT_2:83

for b₁, b₂ being Element of REAL
for b₃ being one-to-one PartFunc of REAL , REAL st b₃ is_increasing_on [.b₁,b₂.] holds
(b₃ | [.b₁,b₂.]) " is_increasing_on b₃ .: [.b₁,b₂.]

proof end;

theorem Th84: :: RFUNCT_2:84

for b₁, b₂ being Element of REAL
for b₃ being one-to-one PartFunc of REAL , REAL st b₃ is_decreasing_on [.b₁,b₂.] holds
(b₃ | [.b₁,b₂.]) " is_decreasing_on b₃ .: [.b₁,b₂.]

proof end;