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


begin

definition
let f be Relation;
attrf is complex-valued  means :Def1: :: VALUED_0:def 1
 rng f c= COMPLEX ;
attrf is ext-real-valued  means :Def2: :: VALUED_0:def 2
 rng f c= ExtREAL ;
attrf is real-valued  means :Def3: :: VALUED_0:def 3
 rng f c= REAL ;
canceled;
canceled;
attrf 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  VALUED_0:def_4_:_
canceled;

:: deftheorem  VALUED_0:def_5_:_
canceled;

:: 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  ->  INT -valued for set ;
coherence
 for b1 being Relation st b1 is natural-valued holds
b1 is INT -valued
proofend;
cluster Relation-like INT -valued  ->  RAT -valued for set ;
coherence
 for b1 being Relation st b1 is INT -valued holds
b1 is RAT -valued
proofend;
cluster Relation-like INT -valued  ->  real-valued for set ;
coherence
 for b1 being Relation st b1 is INT -valued holds
b1 is real-valued
proofend;
cluster Relation-like RAT -valued  ->  real-valued for set ;
coherence
 for b1 being Relation st b1 is RAT -valued holds
b1 is real-valued
proofend;
cluster Relation-like real-valued  ->  ext-real-valued for set ;
coherence
 for b1 being Relation st b1 is real-valued holds
b1 is ext-real-valued
proofend;
cluster Relation-like real-valued  ->  complex-valued for set ;
coherence
 for b1 being Relation st b1 is real-valued holds
b1 is complex-valued
proofend;
cluster Relation-like natural-valued  ->  RAT -valued for set ;
coherence
 for b1 being Relation st b1 is natural-valued holds
b1 is RAT -valued
proofend;
cluster Relation-like natural-valued  ->  real-valued for set ;
coherence
 for b1 being Relation st b1 is natural-valued holds
b1 is real-valued
proofend;
end;

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

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

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

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

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

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

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

registration
let R be natural-valued Relation;
cluster rng R ->  natural-membered ;
coherence
 rng R is natural-membered
proofend;
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
proofend;

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

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

theorem :: VALUED_0:4
for R being Relation
for S being RAT -valued Relation st R c= S holds
R is RAT -valued ;

theorem :: VALUED_0:5
for R being Relation
for S being INT -valued Relation st R c= S holds
R is INT -valued ;

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

registration
let R be complex-valued Relation;
cluster  ->  complex-valued for 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 for 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 for Element of bool R;
coherence
 for b1 being Subset of R holds b1 is real-valued by Th3;
end;

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

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

registration
let R be natural-valued Relation;
cluster  ->  natural-valued for 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;
clusterR \/ S ->  complex-valued ;
coherence
 R \/ S is complex-valued
proofend;
end;

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

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

registration
let R, S be RAT -valued Relation;
clusterR \/ S ->  RAT -valued ;
coherence
 R \/ S is RAT -valued ;
end;

registration
let R, S be INT -valued Relation;
clusterR \/ S ->  INT -valued ;
coherence
 R \/ S is INT -valued ;
end;

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

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

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

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

registration
let R be RAT -valued Relation;
let S be Relation;
clusterR /\ S ->  RAT -valued ;
coherence
 R /\ S is RAT -valued ;
clusterR \ S ->  RAT -valued ;
coherence
 R \ S is RAT -valued ;
end;

registration
let R be INT -valued Relation;
let S be Relation;
clusterR /\ S ->  INT -valued ;
coherence
 R /\ S is INT -valued ;
clusterR \ S ->  INT -valued ;
coherence
 R \ S is INT -valued ;
end;

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

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

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

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

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

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

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

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

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

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

registration
let R be RAT -valued Relation;
let X be set ;
clusterR .: X ->  rational-membered ;
coherence
 R .: X is rational-membered
proofend;
end;

registration
let R be INT -valued Relation;
let X be set ;
clusterR .: X ->  integer-membered ;
coherence
 R .: X is integer-membered
proofend;
end;

registration
let R be natural-valued Relation;
let X be set ;
clusterR .: X ->  natural-membered ;
coherence
 R .: X is natural-membered
proofend;
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 RAT -valued Relation;
let x be set ;
cluster Im (R,x) ->  rational-membered ;
coherence
 Im (R,x) is rational-membered ;
end;

registration
let R be INT -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 ;
clusterR | X ->  complex-valued ;
coherence
 R | X is complex-valued
proofend;
end;

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

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

registration
let R be RAT -valued Relation;
let X be set ;
clusterR | X ->  RAT -valued ;
coherence
 R | X is RAT -valued ;
end;

registration
let R be INT -valued Relation;
let X be set ;
clusterR | X ->  INT -valued ;
coherence
 R | X is INT -valued ;
end;

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

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

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

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

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

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

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

registration
let R be Relation;
let S be complex-valued Relation;
clusterR * S ->  complex-valued ;
coherence
 R * S is complex-valued
proofend;
end;

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

registration
let R be Relation;
let S be real-valued Relation;
clusterR * S ->  real-valued ;
coherence
 R * S is real-valued
proofend;
end;

registration
let R be Relation;
let S be RAT -valued Relation;
clusterR * S ->  RAT -valued ;
coherence
 R * S is RAT -valued ;
end;

registration
let R be Relation;
let S be INT -valued Relation;
clusterR * S ->  INT -valued ;
coherence
 R * S is INT -valued ;
end;

registration
let R be Relation;
let S be natural-valued Relation;
clusterR * S ->  natural-valued ;
coherence
 R * S is natural-valued
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
canceled;
canceled;
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 )
proofend;
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  VALUED_0:def_10_:_
canceled;

:: deftheorem  VALUED_0:def_11_:_
canceled;

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

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

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

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

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

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

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

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

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

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

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

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

registration
let X be set ;
let x be complex number ;
clusterX --> x ->  complex-valued ;
coherence
 X --> x is complex-valued
proofend;
end;

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

registration
let X be set ;
let x be real number ;
clusterX --> x ->  real-valued ;
coherence
 X --> x is real-valued
proofend;
end;

registration
let X be set ;
let x be rational number ;
clusterX --> x ->  RAT -valued ;
coherence
 X --> x is RAT -valued
proofend;
end;

registration
let X be set ;
let x be integer number ;
clusterX --> x ->  INT -valued ;
coherence
 X --> x is INT -valued
proofend;
end;

registration
let X be set ;
let x be Nat;
clusterX --> x ->  natural-valued ;
coherence
 X --> x is natural-valued
proofend;
end;

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

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

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

registration
let f, g be RAT -valued Function;
clusterf +* g ->  RAT -valued ;
coherence
 f +* g is RAT -valued
proofend;
end;

registration
let f, g be INT -valued Function;
clusterf +* g ->  INT -valued ;
coherence
 f +* g is INT -valued
proofend;
end;

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

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

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

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

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

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

registration
let x be set ;
let y be Nat;
clusterx .--> y ->  natural-valued ;
coherence
 x .--> y is natural-valued ;
end;

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

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

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

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

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

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

registration
let X be set ;
let Y be complex-membered set ;
cluster[:X,Y:] ->  complex-valued ;
coherence
 [:X,Y:] is complex-valued
proofend;
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
proofend;
end;

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

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

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

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

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

registration
cluster non empty Relation-like RAT -valued INT -valued Function-like constant natural-valued for set ;
existence
 ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is natural-valued & b1 is INT -valued & b1 is RAT -valued )
proofend;
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
proofend;

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

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

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

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

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

begin

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

:: 2008.08.31, A.T.
registration
cluster trivial Relation-like Function-like ext-real-valued  ->  ext-real-valued increasing decreasing for set ;
coherence
 for b1 being ext-real-valued Function st b1 is trivial holds
( b1 is increasing &amp; b1 is decreasing )
proofend;
end;

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

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

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

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

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

registration
let f be ext-real-valued decreasing Function;
let g be ext-real-valued increasing Function;
clusterf * g ->  decreasing ;
coherence
 g * f is decreasing
proofend;
clusterg * f ->  decreasing ;
coherence
 f * g is decreasing
proofend;
end;

registration
let f be ext-real-valued non-increasing Function;
let g be ext-real-valued non-decreasing Function;
clusterf * g ->  non-increasing ;
coherence
 g * f is non-increasing
proofend;
clusterg * f ->  non-increasing ;
coherence
 f * g is non-increasing
proofend;
end;

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

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

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

:: deftheorem Def17 defines subsequence VALUED_0:def_17_:_
 for s, b2 being ManySortedSet of NAT holds
( b2 is subsequence of s iff ex N being increasing sequence of NAT st b2 = s * N );

Lm1:  for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M
proofend;

registration
let X be non empty set ;
let s be X -valued ManySortedSet of NAT ;
cluster  -> X -valued for subsequence of s;
coherence
 for b1 being subsequence of s holds b1 is X -valued
proofend;
end;

definition
let X be non empty set ;
let s be sequence of X;
:: original:subsequence
redefine mode subsequence of s ->  sequence of X;
coherence
 for b1 being subsequence of s holds b1 is sequence of X
proofend;
end;

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

theorem :: VALUED_0:19
for XX being non empty set
for ss being sequence of XX holds ss is subsequence of ss
proofend;

theorem :: VALUED_0:20
for XX being non empty set
for ss1, ss2, ss3 being sequence of XX st ss1 is subsequence of ss2 &amp; ss2 is subsequence of ss3 holds
ss1 is subsequence of ss3
proofend;

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

theorem Th21: :: VALUED_0:21
for XX being non empty set
for ss being sequence of XX
for ss1 being subsequence of ss holds rng ss1 c= rng ss
proofend;

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

:: from FRECHET2, 2008.09.08, A.T.
definition
let X be non empty set ;
let N be increasing sequence of NAT;
let s be sequence of X;
:: original:*
redefine funcs * N ->  subsequence of s;
correctness
coherence
N * s is subsequence of s;
by Def17;
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 &amp; s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
proofend;

:: to be generalized
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 for Element of bool [:NAT,X:];
existence
 ex b1 being sequence of X st b1 is non-empty
proofend;
end;

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

definition
let X be non empty set ;
let s be sequence of X;
:: original:constant
redefine attrs 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 )
proofend;
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
proofend;

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 V29()
proofend;

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 V29()
proofend;

theorem :: VALUED_0:26
for X being non empty set
for s, s1 being sequence of X st s is V29() &amp; s1 is subsequence of s holds
s = s1
proofend;

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

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

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

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

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

definition
let f be ext-real-valued Function;
attrf 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 );

:: new, 2009.02.03, A.T.
registration
cluster Relation-like COMPLEX -valued  ->  complex-valued for set ;
coherence
 for b1 being Relation st b1 is COMPLEX -valued holds
b1 is complex-valued
proofend;
cluster Relation-like ExtREAL -valued  ->  ext-real-valued for set ;
coherence
 for b1 being Relation st b1 is ExtREAL -valued holds
b1 is ext-real-valued
proofend;
cluster Relation-like REAL -valued  ->  real-valued for set ;
coherence
 for b1 being Relation st b1 is REAL -valued holds
b1 is real-valued
proofend;
cluster Relation-like NAT -valued  ->  natural-valued for set ;
coherence
 for b1 being Relation st b1 is NAT -valued holds
b1 is natural-valued
proofend;
end;

definition
let s be ManySortedSet of NAT ;
redefine attr s is constant  means :: VALUED_0:def 20
 ex x being set st
for n being Nat holds s . n = x;
compatibility
 ( s is constant iff ex x being set st
for n being Nat holds s . n = x )
proofend;
end;

:: deftheorem  defines constant VALUED_0:def_20_:_
 for s being ManySortedSet of NAT holds
( s is constant iff ex x being set st
for n being Nat holds s . n = x );

theorem :: VALUED_0:32
for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M by Lm1;

registration
let X be set ;
cluster Relation-like X -defined Function-like total natural-valued for set ;
existence
 ex b1 being ManySortedSet of X st b1 is natural-valued
proofend;
end;