:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007 Association of Mizar Users


begin

definition
let f be Relation;
attr f is complex-valued means :Def1: :: VALUED_0:def 1
rng f c= COMPLEX ;
attr f is ext-real-valued means :Def2: :: VALUED_0:def 2
rng f c= ExtREAL ;
attr f is real-valued means :Def3: :: VALUED_0:def 3
rng f c= REAL ;
attr f is rational-valued means :Def4: :: VALUED_0:def 4
rng f c= RAT ;
attr f is integer-valued means :Def5: :: VALUED_0:def 5
rng f c= INT ;
attr f is natural-valued means :Def6: :: VALUED_0:def 6
rng f c= NAT ;
end;

:: deftheorem Def1 defines complex-valued VALUED_0:def 1 :
for f being Relation holds
( f is complex-valued iff rng f c= COMPLEX );

:: deftheorem Def2 defines ext-real-valued VALUED_0:def 2 :
for f being Relation holds
( f is ext-real-valued iff rng f c= ExtREAL );

:: deftheorem Def3 defines real-valued VALUED_0:def 3 :
for f being Relation holds
( f is real-valued iff rng f c= REAL );

:: deftheorem Def4 defines rational-valued VALUED_0:def 4 :
for f being Relation holds
( f is rational-valued iff rng f c= RAT );

:: deftheorem Def5 defines integer-valued VALUED_0:def 5 :
for f being Relation holds
( f is integer-valued iff rng f c= INT );

:: deftheorem Def6 defines natural-valued VALUED_0:def 6 :
for f being Relation holds
( f is natural-valued iff rng f c= NAT );

registration
cluster Relation-like natural-valued -> integer-valued set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is integer-valued
proof end;
cluster Relation-like integer-valued -> rational-valued set ;
coherence
for b1 being Relation st b1 is integer-valued holds
b1 is rational-valued
proof end;
cluster Relation-like rational-valued -> real-valued set ;
coherence
for b1 being Relation st b1 is rational-valued holds
b1 is real-valued
proof end;
cluster Relation-like real-valued -> ext-real-valued set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is ext-real-valued
proof end;
cluster Relation-like real-valued -> complex-valued set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is complex-valued
proof end;
end;

registration
cluster empty Relation-like -> natural-valued set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is natural-valued
proof end;
end;

registration
cluster Relation-like Function-like natural-valued set ;
existence
ex b1 being Function st b1 is natural-valued
proof end;
end;

registration
let R be complex-valued Relation;
cluster proj2 R -> complex-membered ;
coherence
rng R is complex-membered
proof end;
end;

registration
let R be ext-real-valued Relation;
cluster proj2 R -> ext-real-membered ;
coherence
rng R is ext-real-membered
proof end;
end;

registration
let R be real-valued Relation;
cluster proj2 R -> real-membered ;
coherence
rng R is real-membered
proof end;
end;

registration
let R be rational-valued Relation;
cluster proj2 R -> rational-membered ;
coherence
rng R is rational-membered
proof end;
end;

registration
let R be integer-valued Relation;
cluster proj2 R -> integer-membered ;
coherence
rng R is integer-membered
proof end;
end;

registration
let R be natural-valued Relation;
cluster proj2 R -> natural-membered ;
coherence
rng R is natural-membered
proof end;
end;

theorem Th1: :: VALUED_0:1
for R being Relation
for S being complex-valued Relation st R c= S holds
R is complex-valued
proof end;

theorem Th2: :: VALUED_0:2
for R being Relation
for S being ext-real-valued Relation st R c= S holds
R is ext-real-valued
proof end;

theorem Th3: :: VALUED_0:3
for R being Relation
for S being real-valued Relation st R c= S holds
R is real-valued
proof end;

theorem Th4: :: VALUED_0:4
for R being Relation
for S being rational-valued Relation st R c= S holds
R is rational-valued
proof end;

theorem Th5: :: VALUED_0:5
for R being Relation
for S being integer-valued Relation st R c= S holds
R is integer-valued
proof end;

theorem Th6: :: VALUED_0:6
for R being Relation
for S being natural-valued Relation st R c= S holds
R is natural-valued
proof end;

registration
let R be complex-valued Relation;
cluster -> complex-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is complex-valued
by Th1;
end;

registration
let R be ext-real-valued Relation;
cluster -> ext-real-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is ext-real-valued
by Th2;
end;

registration
let R be real-valued Relation;
cluster -> real-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is real-valued
by Th3;
end;

registration
let R be rational-valued Relation;
cluster -> rational-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is rational-valued
by Th4;
end;

registration
let R be integer-valued Relation;
cluster -> integer-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is integer-valued
by Th5;
end;

registration
let R be natural-valued Relation;
cluster -> natural-valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is natural-valued
by Th6;
end;

registration
let R, S be complex-valued Relation;
cluster R \/ S -> complex-valued ;
coherence
R \/ S is complex-valued
proof end;
end;

registration
let R, S be ext-real-valued Relation;
cluster R \/ S -> ext-real-valued ;
coherence
R \/ S is ext-real-valued
proof end;
end;

registration
let R, S be real-valued Relation;
cluster R \/ S -> real-valued ;
coherence
R \/ S is real-valued
proof end;
end;

registration
let R, S be rational-valued Relation;
cluster R \/ S -> rational-valued ;
coherence
R \/ S is rational-valued
proof end;
end;

registration
let R, S be integer-valued Relation;
cluster R \/ S -> integer-valued ;
coherence
R \/ S is integer-valued
proof end;
end;

registration
let R, S be natural-valued Relation;
cluster R \/ S -> natural-valued ;
coherence
R \/ S is natural-valued
proof end;
end;

registration
let R be complex-valued Relation;
let S be Relation;
cluster R /\ S -> complex-valued ;
coherence
R /\ S is complex-valued
proof end;
cluster R \ S -> complex-valued ;
coherence
R \ S is complex-valued
;
end;

registration
let R be ext-real-valued Relation;
let S be Relation;
cluster R /\ S -> ext-real-valued ;
coherence
R /\ S is ext-real-valued
proof end;
cluster R \ S -> ext-real-valued ;
coherence
R \ S is ext-real-valued
;
end;

registration
let R be real-valued Relation;
let S be Relation;
cluster R /\ S -> real-valued ;
coherence
R /\ S is real-valued
proof end;
cluster R \ S -> real-valued ;
coherence
R \ S is real-valued
;
end;

registration
let R be rational-valued Relation;
let S be Relation;
cluster R /\ S -> rational-valued ;
coherence
R /\ S is rational-valued
proof end;
cluster R \ S -> rational-valued ;
coherence
R \ S is rational-valued
;
end;

registration
let R be integer-valued Relation;
let S be Relation;
cluster R /\ S -> integer-valued ;
coherence
R /\ S is integer-valued
proof end;
cluster R \ S -> integer-valued ;
coherence
R \ S is integer-valued
;
end;

registration
let R be natural-valued Relation;
let S be Relation;
cluster R /\ S -> natural-valued ;
coherence
R /\ S is natural-valued
proof end;
cluster R \ S -> natural-valued ;
coherence
R \ S is natural-valued
;
end;

registration
let R, S be complex-valued Relation;
cluster R \+\ S -> complex-valued ;
coherence
R \+\ S is complex-valued
;
end;

registration
let R, S be ext-real-valued Relation;
cluster R \+\ S -> ext-real-valued ;
coherence
R \+\ S is ext-real-valued
;
end;

registration
let R, S be real-valued Relation;
cluster R \+\ S -> real-valued ;
coherence
R \+\ S is real-valued
;
end;

registration
let R, S be rational-valued Relation;
cluster R \+\ S -> rational-valued ;
coherence
R \+\ S is rational-valued
;
end;

registration
let R, S be integer-valued Relation;
cluster R \+\ S -> integer-valued ;
coherence
R \+\ S is integer-valued
;
end;

registration
let R, S be natural-valued Relation;
cluster R \+\ S -> natural-valued ;
coherence
R \+\ S is natural-valued
;
end;

registration
let R be complex-valued Relation;
let X be set ;
cluster R .: X -> complex-membered ;
coherence
R .: X is complex-membered
proof end;
end;

registration
let R be ext-real-valued Relation;
let X be set ;
cluster R .: X -> ext-real-membered ;
coherence
R .: X is ext-real-membered
proof end;
end;

registration
let R be real-valued Relation;
let X be set ;
cluster R .: X -> real-membered ;
coherence
R .: X is real-membered
proof end;
end;

registration
let R be rational-valued Relation;
let X be set ;
cluster R .: X -> rational-membered ;
coherence
R .: X is rational-membered
proof end;
end;

registration
let R be integer-valued Relation;
let X be set ;
cluster R .: X -> integer-membered ;
coherence
R .: X is integer-membered
proof end;
end;

registration
let R be natural-valued Relation;
let X be set ;
cluster R .: X -> natural-membered ;
coherence
R .: X is natural-membered
proof end;
end;

registration
let R be complex-valued Relation;
let x be set ;
cluster Im (R,x) -> complex-membered ;
coherence
Im (R,x) is complex-membered
;
end;

registration
let R be ext-real-valued Relation;
let x be set ;
cluster Im (R,x) -> ext-real-membered ;
coherence
Im (R,x) is ext-real-membered
;
end;

registration
let R be real-valued Relation;
let x be set ;
cluster Im (R,x) -> real-membered ;
coherence
Im (R,x) is real-membered
;
end;

registration
let R be rational-valued Relation;
let x be set ;
cluster Im (R,x) -> rational-membered ;
coherence
Im (R,x) is rational-membered
;
end;

registration
let R be integer-valued Relation;
let x be set ;
cluster Im (R,x) -> integer-membered ;
coherence
Im (R,x) is integer-membered
;
end;

registration
let R be natural-valued Relation;
let x be set ;
cluster Im (R,x) -> natural-membered ;
coherence
Im (R,x) is natural-membered
;
end;

registration
let R be complex-valued Relation;
let X be set ;
cluster R | X -> complex-valued ;
coherence
R | X is complex-valued
proof end;
end;

registration
let R be ext-real-valued Relation;
let X be set ;
cluster R | X -> ext-real-valued ;
coherence
R | X is ext-real-valued
proof end;
end;

registration
let R be real-valued Relation;
let X be set ;
cluster R | X -> real-valued ;
coherence
R | X is real-valued
proof end;
end;

registration
let R be rational-valued Relation;
let X be set ;
cluster R | X -> rational-valued ;
coherence
R | X is rational-valued
proof end;
end;

registration
let R be integer-valued Relation;
let X be set ;
cluster R | X -> integer-valued ;
coherence
R | X is integer-valued
proof end;
end;

registration
let R be natural-valued Relation;
let X be set ;
cluster R | X -> natural-valued ;
coherence
R | X is natural-valued
proof end;
end;

registration
let X be complex-membered set ;
cluster id X -> complex-valued ;
coherence
id X is complex-valued
proof end;
end;

registration
let X be ext-real-membered set ;
cluster id X -> ext-real-valued ;
coherence
id X is ext-real-valued
proof end;
end;

registration
let X be real-membered set ;
cluster id X -> real-valued ;
coherence
id X is real-valued
proof end;
end;

registration
let X be rational-membered set ;
cluster id X -> rational-valued ;
coherence
id X is rational-valued
proof end;
end;

registration
let X be integer-membered set ;
cluster id X -> integer-valued ;
coherence
id X is integer-valued
proof end;
end;

registration
let X be natural-membered set ;
cluster id X -> natural-valued ;
coherence
id X is natural-valued
proof end;
end;

registration
let R be Relation;
let S be complex-valued Relation;
cluster R * S -> complex-valued ;
coherence
R * S is complex-valued
proof end;
end;

registration
let R be Relation;
let S be ext-real-valued Relation;
cluster R * S -> ext-real-valued ;
coherence
R * S is ext-real-valued
proof end;
end;

registration
let R be Relation;
let S be real-valued Relation;
cluster R * S -> real-valued ;
coherence
R * S is real-valued
proof end;
end;

registration
let R be Relation;
let S be rational-valued Relation;
cluster R * S -> rational-valued ;
coherence
R * S is rational-valued
proof end;
end;

registration
let R be Relation;
let S be integer-valued Relation;
cluster R * S -> integer-valued ;
coherence
R * S is integer-valued
proof end;
end;

registration
let R be Relation;
let S be natural-valued Relation;
cluster R * S -> natural-valued ;
coherence
R * S is natural-valued
proof end;
end;

definition
let f be Function;
redefine attr f is complex-valued means :Def7: :: VALUED_0:def 7
for x being set st x in dom f holds
f . x is complex ;
compatibility
( f is complex-valued iff for x being set st x in dom f holds
f . x is complex )
proof end;
redefine attr f is ext-real-valued means :Def8: :: VALUED_0:def 8
for x being set st x in dom f holds
f . x is ext-real ;
compatibility
( f is ext-real-valued iff for x being set st x in dom f holds
f . x is ext-real )
proof end;
redefine attr f is real-valued means :Def9: :: VALUED_0:def 9
for x being set st x in dom f holds
f . x is real ;
compatibility
( f is real-valued iff for x being set st x in dom f holds
f . x is real )
proof end;
redefine attr f is rational-valued means :Def10: :: VALUED_0:def 10
for x being set st x in dom f holds
f . x is rational ;
compatibility
( f is rational-valued iff for x being set st x in dom f holds
f . x is rational )
proof end;
redefine attr f is integer-valued means :Def11: :: VALUED_0:def 11
for x being set st x in dom f holds
f . x is integer ;
compatibility
( f is integer-valued iff for x being set st x in dom f holds
f . x is integer )
proof end;
redefine attr f is natural-valued means :Def12: :: VALUED_0:def 12
for x being set st x in dom f holds
f . x is natural ;
compatibility
( f is natural-valued iff for x being set st x in dom f holds
f . x is natural )
proof end;
end;

:: deftheorem Def7 defines complex-valued VALUED_0:def 7 :
for f being Function holds
( f is complex-valued iff for x being set st x in dom f holds
f . x is complex );

:: deftheorem Def8 defines ext-real-valued VALUED_0:def 8 :
for f being Function holds
( f is ext-real-valued iff for x being set st x in dom f holds
f . x is ext-real );

:: deftheorem Def9 defines real-valued VALUED_0:def 9 :
for f being Function holds
( f is real-valued iff for x being set st x in dom f holds
f . x is real );

:: deftheorem Def10 defines rational-valued VALUED_0:def 10 :
for f being Function holds
( f is rational-valued iff for x being set st x in dom f holds
f . x is rational );

:: deftheorem Def11 defines integer-valued VALUED_0:def 11 :
for f being Function holds
( f is integer-valued iff for x being set st x in dom f holds
f . x is integer );

:: deftheorem Def12 defines natural-valued VALUED_0:def 12 :
for f being Function holds
( f is natural-valued iff for x being set st x in dom f holds
f . x is natural );

theorem Th7: :: VALUED_0:7
for f being Function holds
( f is complex-valued iff for x being set holds f . x is complex )
proof end;

theorem Th8: :: VALUED_0:8
for f being Function holds
( f is ext-real-valued iff for x being set holds f . x is ext-real )
proof end;

theorem Th9: :: VALUED_0:9
for f being Function holds
( f is real-valued iff for x being set holds f . x is real )
proof end;

theorem Th10: :: VALUED_0:10
for f being Function holds
( f is rational-valued iff for x being set holds f . x is rational )
proof end;

theorem Th11: :: VALUED_0:11
for f being Function holds
( f is integer-valued iff for x being set holds f . x is integer )
proof end;

theorem Th12: :: VALUED_0:12
for f being Function holds
( f is natural-valued iff for x being set holds f . x is natural )
proof end;

registration
let f be complex-valued Function;
let x be set ;
cluster f . x -> complex ;
coherence
f . x is complex
by Th7;
end;

registration
let f be ext-real-valued Function;
let x be set ;
cluster f . x -> ext-real ;
coherence
f . x is ext-real
by Th8;
end;

registration
let f be real-valued Function;
let x be set ;
cluster f . x -> real ;
coherence
f . x is real
by Th9;
end;

registration
let f be rational-valued Function;
let x be set ;
cluster f . x -> rational ;
coherence
f . x is rational
by Th10;
end;

registration
let f be integer-valued Function;
let x be set ;
cluster f . x -> integer ;
coherence
f . x is integer
by Th11;
end;

registration
let f be natural-valued Function;
let x be set ;
cluster f . x -> natural ;
coherence
f . x is natural
by Th12;
end;

registration
let X be set ;
let x be complex number ;
cluster X --> x -> complex-valued ;
coherence
X --> x is complex-valued
proof end;
end;

registration
let X be set ;
let x be ext-real number ;
cluster X --> x -> ext-real-valued ;
coherence
X --> x is ext-real-valued
proof end;
end;

registration
let X be set ;
let x be real number ;
cluster X --> x -> real-valued ;
coherence
X --> x is real-valued
proof end;
end;

registration
let X be set ;
let x be rational number ;
cluster X --> x -> rational-valued ;
coherence
X --> x is rational-valued
proof end;
end;

registration
let X be set ;
let x be integer number ;
cluster X --> x -> integer-valued ;
coherence
X --> x is integer-valued
proof end;
end;

registration
let X be set ;
let x be natural number ;
cluster X --> x -> natural-valued ;
coherence
X --> x is natural-valued
proof end;
end;

registration
let f, g be complex-valued Function;
cluster f +* g -> complex-valued ;
coherence
f +* g is complex-valued
proof end;
end;

registration
let f, g be ext-real-valued Function;
cluster f +* g -> ext-real-valued ;
coherence
f +* g is ext-real-valued
proof end;
end;

registration
let f, g be real-valued Function;
cluster f +* g -> real-valued ;
coherence
f +* g is real-valued
proof end;
end;

registration
let f, g be rational-valued Function;
cluster f +* g -> rational-valued ;
coherence
f +* g is rational-valued
proof end;
end;

registration
let f, g be integer-valued Function;
cluster f +* g -> integer-valued ;
coherence
f +* g is integer-valued
proof end;
end;

registration
let f, g be natural-valued Function;
cluster f +* g -> natural-valued ;
coherence
f +* g is natural-valued
proof end;
end;

registration
let x be set ;
let y be complex number ;
cluster x .--> y -> complex-valued ;
coherence
x .--> y is complex-valued
;
end;

registration
let x be set ;
let y be ext-real number ;
cluster x .--> y -> ext-real-valued ;
coherence
x .--> y is ext-real-valued
;
end;

registration
let x be set ;
let y be real number ;
cluster x .--> y -> real-valued ;
coherence
x .--> y is real-valued
;
end;

registration
let x be set ;
let y be rational number ;
cluster x .--> y -> rational-valued ;
coherence
x .--> y is rational-valued
;
end;

registration
let x be set ;
let y be integer number ;
cluster x .--> y -> integer-valued ;
coherence
x .--> y is integer-valued
;
end;

registration
let x be set ;
let y be natural number ;
cluster x .--> y -> natural-valued ;
coherence
x .--> y is natural-valued
;
end;

registration
let X be set ;
let Y be complex-membered set ;
cluster -> complex-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is complex-valued
proof end;
end;

registration
let X be set ;
let Y be ext-real-membered set ;
cluster -> ext-real-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is ext-real-valued
proof end;
end;

registration
let X be set ;
let Y be real-membered set ;
cluster -> real-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is real-valued
proof end;
end;

registration
let X be set ;
let Y be rational-membered set ;
cluster -> rational-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is rational-valued
proof end;
end;

registration
let X be set ;
let Y be integer-membered set ;
cluster -> integer-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is integer-valued
proof end;
end;

registration
let X be set ;
let Y be natural-membered set ;
cluster -> natural-valued Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is natural-valued
proof end;
end;

registration
let X be set ;
let Y be complex-membered set ;
cluster [:X,Y:] -> complex-valued ;
coherence
[:X,Y:] is complex-valued
proof end;
end;

registration
let X be set ;
let Y be ext-real-membered set ;
cluster [:X,Y:] -> ext-real-valued ;
coherence
[:X,Y:] is ext-real-valued
proof end;
end;

registration
let X be set ;
let Y be real-membered set ;
cluster [:X,Y:] -> real-valued ;
coherence
[:X,Y:] is real-valued
proof end;
end;

registration
let X be set ;
let Y be rational-membered set ;
cluster [:X,Y:] -> rational-valued ;
coherence
[:X,Y:] is rational-valued
proof end;
end;

registration
let X be set ;
let Y be integer-membered set ;
cluster [:X,Y:] -> integer-valued ;
coherence
[:X,Y:] is integer-valued
proof end;
end;

registration
let X be set ;
let Y be natural-membered set ;
cluster [:X,Y:] -> natural-valued ;
coherence
[:X,Y:] is natural-valued
proof end;
end;

notation
let f be ext-real-valued Relation;
synonym non-zero f for non-empty ;
end;

registration
cluster non empty Relation-like Function-like constant natural-valued set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is natural-valued )
proof end;
end;

theorem :: VALUED_0:13
for f being non empty constant complex-valued Function ex r being complex number st
for x being set st x in dom f holds
f . x = r
proof end;

theorem :: VALUED_0:14
for f being non empty constant ext-real-valued Function ex r being ext-real number st
for x being set st x in dom f holds
f . x = r
proof end;

theorem :: VALUED_0:15
for f being non empty constant real-valued Function ex r being real number st
for x being set st x in dom f holds
f . x = r
proof end;

theorem :: VALUED_0:16
for f being non empty constant rational-valued Function ex r being rational number st
for x being set st x in dom f holds
f . x = r
proof end;

theorem :: VALUED_0:17
for f being non empty constant integer-valued Function ex r being integer number st
for x being set st x in dom f holds
f . x = r
proof end;

theorem :: VALUED_0:18
for f being non empty constant natural-valued Function ex r being natural number st
for x being set st x in dom f holds
f . x = r
proof end;

begin

definition
let f be ext-real-valued Function;
attr f is increasing means :Def13: :: VALUED_0:def 13
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2;
attr f is decreasing means :Def14: :: VALUED_0:def 14
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2;
attr f is non-decreasing means :Def15: :: VALUED_0:def 15
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2;
attr f is non-increasing means :Def16: :: VALUED_0:def 16
for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2;
end;

:: deftheorem Def13 defines increasing VALUED_0:def 13 :
for f being ext-real-valued Function holds
( f is increasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2 );

:: deftheorem Def14 defines decreasing VALUED_0:def 14 :
for f being ext-real-valued Function holds
( f is decreasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2 );

:: deftheorem Def15 defines non-decreasing VALUED_0:def 15 :
for f being ext-real-valued Function holds
( f is non-decreasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2 );

:: deftheorem Def16 defines non-increasing VALUED_0:def 16 :
for f being ext-real-valued Function holds
( f is non-increasing iff for e1, e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2 );

registration
cluster trivial Relation-like Function-like ext-real-valued -> ext-real-valued increasing decreasing set ;
coherence
for b1 being ext-real-valued Function st b1 is trivial holds
( b1 is increasing & b1 is decreasing )
proof end;
end;

registration
cluster Relation-like Function-like ext-real-valued increasing -> ext-real-valued non-decreasing set ;
coherence
for b1 being ext-real-valued Function st b1 is increasing holds
b1 is non-decreasing
proof end;
cluster Relation-like Function-like ext-real-valued decreasing -> ext-real-valued non-increasing set ;
coherence
for b1 being ext-real-valued Function st b1 is decreasing holds
b1 is non-increasing
proof end;
end;

registration
let f, g be ext-real-valued increasing Function;
cluster f * g -> increasing ;
coherence
g * f is increasing
proof end;
end;

registration
let f, g be ext-real-valued non-decreasing Function;
cluster f * g -> non-decreasing ;
coherence
g * f is non-decreasing
proof end;
end;

registration
let f, g be ext-real-valued decreasing Function;
cluster f * g -> increasing ;
coherence
g * f is increasing
proof end;
end;

registration
let f, g be ext-real-valued non-increasing Function;
cluster f * g -> non-decreasing ;
coherence
g * f is non-decreasing
proof end;
end;

registration
let f be ext-real-valued decreasing Function;
let g be ext-real-valued increasing Function;
cluster f * g -> decreasing ;
coherence
g * f is decreasing
proof end;
cluster g * f -> decreasing ;
coherence
f * g is decreasing
proof end;
end;

registration
let f be ext-real-valued non-increasing Function;
let g be ext-real-valued non-decreasing Function;
cluster f * g -> non-increasing ;
coherence
g * f is non-increasing
proof end;
cluster g * f -> non-increasing ;
coherence
f * g is non-increasing
proof end;
end;

registration
let X be ext-real-membered set ;
cluster id X -> increasing Function of X,X;
coherence
for b1 being Function of X,X st b1 = id X holds
b1 is increasing
proof end;
end;

registration
cluster non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued increasing Element of bool [:NAT,NAT:];
existence
ex b1 being sequence of NAT st b1 is increasing
proof end;
end;

definition
let X be set ;
let s be sequence of X;
mode subsequence of s -> sequence of X means :Def17: :: VALUED_0:def 17
ex N being increasing sequence of NAT st it = s * N;
existence
ex b1 being sequence of X ex N being increasing sequence of NAT st b1 = s * N
proof end;
end;

:: deftheorem Def17 defines subsequence VALUED_0:def 17 :
for X being set
for s, b3 being sequence of X holds
( b3 is subsequence of s iff ex N being increasing sequence of NAT st b3 = s * N );

definition
let X be non empty set ;
let s be sequence of X;
let k be Nat;
:: original: ^\
redefine func s ^\ k -> subsequence of s;
coherence
s ^\ k is subsequence of s
proof end;
end;

theorem :: VALUED_0:19
for X being set
for s being sequence of X holds s is subsequence of s
proof end;

theorem :: VALUED_0:20
for X being set
for s1, s2, s3 being sequence of X st s1 is subsequence of s2 & s2 is subsequence of s3 holds
s1 is subsequence of s3
proof end;

registration
let X be set ;
cluster Relation-like NAT -defined X -valued Function-like constant quasi_total Element of bool [:NAT,X:];
existence
ex b1 being sequence of X st b1 is constant
proof end;
end;

theorem Th21: :: VALUED_0:21
for X being set
for s being sequence of X
for s1 being subsequence of s holds rng s1 c= rng s
proof end;

registration
let X be set ;
let s be constant sequence of X;
cluster -> constant subsequence of s;
coherence
for b1 being subsequence of s holds b1 is constant
proof end;
end;

definition
let X be set ;
let N be increasing sequence of NAT;
let s be sequence of X;
:: original: *
redefine func s * N -> subsequence of s;
correctness
coherence
N * s is subsequence of s
;
proof end;
end;

theorem :: VALUED_0:22
for X, Y being non empty set
for s, s1 being sequence of X
for h being PartFunc of X,Y st rng s c= dom h & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
proof end;

registration
let X be with_non-empty_element set ;
cluster non empty Relation-like non-empty NAT -defined X -valued Function-like total quasi_total Element of bool [:NAT,X:];
existence
ex b1 being sequence of X st b1 is non-zero
proof end;
end;

registration
let X be with_non-empty_element set ;
let s be non-empty sequence of X;
cluster -> non-empty subsequence of s;
coherence
for b1 being subsequence of s holds b1 is non-zero
proof end;
end;

definition
let X be non empty set ;
let s be sequence of X;
:: original: constant
redefine attr s is constant means :: VALUED_0:def 18
ex x being Element of X st
for n being Nat holds s . n = x;
compatibility
( s is constant iff ex x being Element of X st
for n being Nat holds s . n = x )
proof end;
end;

:: deftheorem defines constant VALUED_0:def 18 :
for X being non empty set
for s being sequence of X holds
( s is constant iff ex x being Element of X st
for n being Nat holds s . n = x );

theorem Th23: :: VALUED_0:23
for i, j being Nat
for X being set
for s being constant sequence of X holds s . i = s . j
proof end;

theorem Th24: :: VALUED_0:24
for X being non empty set
for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is constant
proof end;

theorem :: VALUED_0:25
for X being non empty set
for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is constant
proof end;

theorem :: VALUED_0:26
for X being non empty set
for s, s1 being sequence of X st s is constant & s1 is subsequence of s holds
s = s1
proof end;

theorem Th27: :: VALUED_0:27
for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
proof end;

theorem Th28: :: VALUED_0:28
for X being non empty set
for s being sequence of X
for n being Nat holds s . n in rng s
proof end;

theorem :: VALUED_0:29
for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
proof end;

theorem Th30: :: VALUED_0:30
for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y st rng s c= dom h holds
h .: (rng s) = rng (h /* s)
proof end;

theorem :: VALUED_0:31
for X, Y being non empty set
for Z being set
for s being sequence of X
for h1 being PartFunc of X,Y
for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
proof end;

definition
let f be ext-real-valued Function;
attr f is zeroed means :: VALUED_0:def 19
f . {} = 0 ;
end;

:: deftheorem defines zeroed VALUED_0:def 19 :
for f being ext-real-valued Function holds
( f is zeroed iff f . {} = 0 );

registration
cluster Relation-like COMPLEX -valued -> complex-valued set ;
coherence
for b1 being Relation st b1 is COMPLEX -valued holds
b1 is complex-valued
proof end;
cluster Relation-like ExtREAL -valued -> ext-real-valued set ;
coherence
for b1 being Relation st b1 is ExtREAL -valued holds
b1 is ext-real-valued
proof end;
cluster Relation-like REAL -valued -> real-valued set ;
coherence
for b1 being Relation st b1 is REAL -valued holds
b1 is real-valued
proof end;
cluster Relation-like RAT -valued -> rational-valued set ;
coherence
for b1 being Relation st b1 is RAT -valued holds
b1 is rational-valued
proof end;
cluster Relation-like INT -valued -> integer-valued set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is integer-valued
proof end;
cluster Relation-like NAT -valued -> natural-valued set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is natural-valued
proof end;
end;