:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-2012 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 ;
canceled;
canceled;
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 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
proof end;
cluster Relation-like INT -valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is RAT -valued
proof end;
cluster Relation-like INT -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is INT -valued holds
b1 is real-valued
proof end;
cluster Relation-like RAT -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is RAT -valued holds
b1 is real-valued
proof end;
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
proof end;
cluster Relation-like real-valued -> complex-valued for set ;
coherence
for b1 being Relation st b1 is real-valued holds
b1 is complex-valued
proof end;
cluster Relation-like natural-valued -> RAT -valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is RAT -valued
proof end;
cluster Relation-like natural-valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is real-valued
proof end;
end;

registration
cluster empty Relation-like -> natural-valued for 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 for set ;
existence
ex b1 being Function st b1 is natural-valued
proof end;
end;

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

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

registration
let R be real-valued Relation;
cluster rng R -> real-membered ;
coherence
rng R is real-membered
proof end;
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
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 :: 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
proof end;

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;
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 RAT -valued Relation;
cluster R \/ S -> RAT -valued ;
coherence
R \/ S is RAT -valued
;
end;

registration
let R, S be INT -valued Relation;
cluster R \/ S -> INT -valued ;
coherence
R \/ S is INT -valued
;
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 RAT -valued Relation;
let S be Relation;
cluster R /\ S -> RAT -valued ;
coherence
R /\ S is RAT -valued
;
cluster R \ S -> RAT -valued ;
coherence
R \ S is RAT -valued
;
end;

registration
let R be INT -valued Relation;
let S be Relation;
cluster R /\ S -> INT -valued ;
coherence
R /\ S is INT -valued
;
cluster R \ S -> INT -valued ;
coherence
R \ S is INT -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 RAT -valued Relation;
cluster R \+\ S -> RAT -valued ;
coherence
R \+\ S is RAT -valued
;
end;

registration
let R, S be INT -valued Relation;
cluster R \+\ S -> INT -valued ;
coherence
R \+\ S is INT -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 RAT -valued Relation;
let X be set ;
cluster R .: X -> rational-membered ;
coherence
R .: X is rational-membered
proof end;
end;

registration
let R be INT -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 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 ;
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 RAT -valued Relation;
let X be set ;
cluster R | X -> RAT -valued ;
coherence
R | X is RAT -valued
;
end;

registration
let R be INT -valued Relation;
let X be set ;
cluster R | X -> INT -valued ;
coherence
R | X is INT -valued
;
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 -> RAT -valued ;
coherence
id X is RAT -valued
proof end;
end;

registration
let X be integer-membered set ;
cluster id X -> INT -valued ;
coherence
id X is INT -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 RAT -valued Relation;
cluster R * S -> RAT -valued ;
coherence
R * S is RAT -valued
;
end;

registration
let R be Relation;
let S be INT -valued Relation;
cluster R * S -> INT -valued ;
coherence
R * S is INT -valued
;
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;
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 )
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 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 )
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 RAT -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 INT -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 RAT -valued Function;
let x be set ;
cluster f . x -> rational ;
coherence
f . x is rational
by Th10;
end;

registration
let f be INT -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 -> RAT -valued ;
coherence
X --> x is RAT -valued
proof end;
end;

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

registration
let X be set ;
let x be Nat;
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 RAT -valued Function;
cluster f +* g -> RAT -valued ;
coherence
f +* g is RAT -valued
proof end;
end;

registration
let f, g be INT -valued Function;
cluster f +* g -> INT -valued ;
coherence
f +* g is INT -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 -> RAT -valued ;
coherence
x .--> y is RAT -valued
;
end;

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

registration
let x be set ;
let y be Nat;
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 for 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 for 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 for 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 -> RAT -valued for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is RAT -valued
proof end;
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
proof end;
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
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:] -> RAT -valued ;
coherence
[:X,Y:] is RAT -valued
proof end;
end;

registration
let X be set ;
let Y be integer-membered set ;
cluster [:X,Y:] -> INT -valued ;
coherence
[:X,Y:] is INT -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 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 )
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 RAT -valued constant 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 INT -valued constant 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 Nat 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 );

:: 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 & b1 is decreasing )
proof end;
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
proof end;
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
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 for 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 natural-valued increasing for Element of bool [:NAT,NAT:];
existence
ex b1 being sequence of NAT st b1 is increasing
proof end;
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
proof end;
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

proof end;

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

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 XX being non empty set
for ss being sequence of XX holds ss is subsequence of ss
proof end;

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

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

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
proof end;
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 func s * 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 & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
proof end;

:: 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
proof end;
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
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 V29()
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 V29()
proof end;

theorem :: VALUED_0:26
for X being non empty set
for s, s1 being sequence of X st s is V29() & 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 );

:: 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
proof end;
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
proof end;
cluster Relation-like REAL -valued -> real-valued for set ;
coherence
for b1 being Relation st b1 is REAL -valued holds
b1 is real-valued
proof end;
cluster Relation-like NAT -valued -> natural-valued for set ;
coherence
for b1 being Relation st b1 is NAT -valued holds
b1 is natural-valued
proof end;
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 )
proof end;
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
proof end;
end;