:: VALUED_0 semantic presentation

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
proof
let R be Relation; ::_thesis: ( R is natural-valued implies R is INT -valued )
assume  rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is INT -valued
hence  rng R c= INT by NUMBERS:17, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is INT -valued implies R is RAT -valued )
assume  rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is RAT -valued
hence  rng R c= RAT by NUMBERS:14, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is INT -valued implies R is real-valued )
assume  rng R c= INT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued
hence  rng R c= REAL by XBOOLE_1:1, NUMBERS:15; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is RAT -valued implies R is real-valued )
assume  rng R c= RAT ; :: according to RELAT_1:def_19 ::_thesis: R is real-valued
hence  rng R c= REAL by NUMBERS:12, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is real-valued implies R is ext-real-valued )
assume  rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is ext-real-valued
hence  rng R c= ExtREAL by NUMBERS:31, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is real-valued implies R is complex-valued )
assume  rng R c= REAL ; :: according to VALUED_0:def_3 ::_thesis: R is complex-valued
hence  rng R c= COMPLEX by NUMBERS:11, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is natural-valued implies R is RAT -valued )
assume  rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is RAT -valued
hence  rng R c= RAT by NUMBERS:18, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is natural-valued implies R is real-valued )
assume  rng R c= NAT ; :: according to VALUED_0:def_6 ::_thesis: R is real-valued
hence  rng R c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is empty implies R is natural-valued )
assume  R is empty ; ::_thesis: R is natural-valued
hence  rng R c= NAT by RELAT_1:38, XBOOLE_1:2; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like natural-valued for set ;
existence
 ex b1 being Function st b1 is natural-valued
proof
take  {} ; ::_thesis: {} is natural-valued
thus  {} is natural-valued ; ::_thesis: verum
end;
end;

registration
let R be complex-valued Relation;
cluster rng R ->  complex-membered ;
coherence
 rng R is complex-membered
proof
 rng R c= COMPLEX by Def1;
hence  rng R is complex-membered ; ::_thesis: verum
end;
end;

registration
let R be ext-real-valued Relation;
cluster rng R ->  ext-real-membered ;
coherence
 rng R is ext-real-membered
proof
 rng R c= ExtREAL by Def2;
hence  rng R is ext-real-membered ; ::_thesis: verum
end;
end;

registration
let R be real-valued Relation;
cluster rng R ->  real-membered ;
coherence
 rng R is real-membered
proof
 rng R c= REAL by Def3;
hence  rng R is real-membered ; ::_thesis: verum
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
 rng R c= NAT by Def6;
hence  rng R is natural-membered ; ::_thesis: verum
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
let R be Relation; ::_thesis: for S being complex-valued Relation st R c= S holds
R is complex-valued
let S be complex-valued Relation; ::_thesis: ( R c= S implies R is complex-valued )
assume  R c= S ; ::_thesis: R is complex-valued
then A1: rng R c= rng S by RELAT_1:11;
 rng S c= COMPLEX by Def1;
hence  rng R c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being ext-real-valued Relation st R c= S holds
R is ext-real-valued
let S be ext-real-valued Relation; ::_thesis: ( R c= S implies R is ext-real-valued )
assume  R c= S ; ::_thesis: R is ext-real-valued
then A1: rng R c= rng S by RELAT_1:11;
 rng S c= ExtREAL by Def2;
hence  rng R c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being real-valued Relation st R c= S holds
R is real-valued
let S be real-valued Relation; ::_thesis: ( R c= S implies R is real-valued )
assume  R c= S ; ::_thesis: R is real-valued
then A1: rng R c= rng S by RELAT_1:11;
 rng S c= REAL by Def3;
hence  rng R c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: for S being natural-valued Relation st R c= S holds
R is natural-valued
let S be natural-valued Relation; ::_thesis: ( R c= S implies R is natural-valued )
assume  R c= S ; ::_thesis: R is natural-valued
then A1: rng R c= rng S by RELAT_1:11;
 rng S c= NAT by Def6;
hence  rng R c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
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;
clusterR \/ S ->  complex-valued ;
coherence
 R \/ S is complex-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
 ( rng R c= COMPLEX & rng S c= COMPLEX ) by Def1;
hence  rng (R \/ S) c= COMPLEX by A1, XBOOLE_1:8; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;

registration
let R, S be ext-real-valued Relation;
clusterR \/ S ->  ext-real-valued ;
coherence
 R \/ S is ext-real-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
 ( rng R c= ExtREAL & rng S c= ExtREAL ) by Def2;
hence  rng (R \/ S) c= ExtREAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;

registration
let R, S be real-valued Relation;
clusterR \/ S ->  real-valued ;
coherence
 R \/ S is real-valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
 ( rng R c= REAL & rng S c= REAL ) by Def3;
hence  rng (R \/ S) c= REAL by A1, XBOOLE_1:8; :: according to VALUED_0:def_3 ::_thesis: verum
end;
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
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
 ( rng R c= NAT & rng S c= NAT ) by Def6;
hence  rng (R \/ S) c= NAT by A1, XBOOLE_1:8; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;

registration
let R be complex-valued Relation;
let S be Relation;
clusterR /\ S ->  complex-valued ;
coherence
 R /\ S is complex-valued
proof
 R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
 rng R c= COMPLEX by Def1;
hence  rng (R /\ S) c= COMPLEX by A1, XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
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
proof
 R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
 rng R c= ExtREAL by Def2;
hence  rng (R /\ S) c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
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
proof
 R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
 rng R c= REAL by Def3;
hence  rng (R /\ S) c= REAL by A1, XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
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
proof
 R /\ S c= R by XBOOLE_1:17;
then A1: rng (R /\ S) c= rng R by RELAT_1:11;
 rng R c= NAT by Def6;
hence  rng (R /\ S) c= NAT by A1, XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
end;
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
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is complex-membered ; ::_thesis: verum
end;
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
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is ext-real-membered ; ::_thesis: verum
end;
end;

registration
let R be real-valued Relation;
let X be set ;
clusterR .: X ->  real-membered ;
coherence
 R .: X is real-membered
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is real-membered ; ::_thesis: verum
end;
end;

registration
let R be RAT -valued Relation;
let X be set ;
clusterR .: X ->  rational-membered ;
coherence
 R .: X is rational-membered
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is rational-membered ; ::_thesis: verum
end;
end;

registration
let R be INT -valued Relation;
let X be set ;
clusterR .: X ->  integer-membered ;
coherence
 R .: X is integer-membered
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is integer-membered ; ::_thesis: verum
end;
end;

registration
let R be natural-valued Relation;
let X be set ;
clusterR .: X ->  natural-membered ;
coherence
 R .: X is natural-membered
proof
 R .: X c= rng R by RELAT_1:111;
hence  R .: X is natural-membered ; ::_thesis: verum
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 ;
clusterR | X ->  complex-valued ;
coherence
 R | X is complex-valued
proof
 ( rng R c= COMPLEX & rng (R | X) c= rng R ) by Def1, RELAT_1:70;
hence  rng (R | X) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
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
proof
 ( rng R c= ExtREAL & rng (R | X) c= rng R ) by Def2, RELAT_1:70;
hence  rng (R | X) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;

registration
let R be real-valued Relation;
let X be set ;
clusterR | X ->  real-valued ;
coherence
 R | X is real-valued
proof
 ( rng R c= REAL & rng (R | X) c= rng R ) by Def3, RELAT_1:70;
hence  rng (R | X) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
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
proof
 ( rng R c= NAT & rng (R | X) c= rng R ) by Def6, RELAT_1:70;
hence  rng (R | X) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;

registration
let X be complex-membered set ;
cluster id X ->  complex-valued ;
coherence
 id X is complex-valued
proof
thus  rng (id X) c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
end;

registration
let X be ext-real-membered set ;
cluster id X ->  ext-real-valued ;
coherence
 id X is ext-real-valued
proof
thus  rng (id X) c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;

registration
let X be real-membered set ;
cluster id X ->  real-valued ;
coherence
 id X is real-valued
proof
thus  rng (id X) c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
end;
end;

registration
let X be rational-membered set ;
cluster id X ->  RAT -valued ;
coherence
 id X is RAT -valued
proof
thus  rng (id X) c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let X be integer-membered set ;
cluster id X ->  INT -valued ;
coherence
 id X is INT -valued
proof
thus  rng (id X) c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let X be natural-membered set ;
cluster id X ->  natural-valued ;
coherence
 id X is natural-valued
proof
thus  rng (id X) c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
end;
end;

registration
let R be Relation;
let S be complex-valued Relation;
clusterR * S ->  complex-valued ;
coherence
 R * S is complex-valued
proof
 ( rng S c= COMPLEX & rng (R * S) c= rng S ) by Def1, RELAT_1:26;
hence  rng (R * S) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def_1 ::_thesis: verum
end;
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
proof
 ( rng S c= ExtREAL & rng (R * S) c= rng S ) by Def2, RELAT_1:26;
hence  rng (R * S) c= ExtREAL by XBOOLE_1:1; :: according to VALUED_0:def_2 ::_thesis: verum
end;
end;

registration
let R be Relation;
let S be real-valued Relation;
clusterR * S ->  real-valued ;
coherence
 R * S is real-valued
proof
 ( rng S c= REAL & rng (R * S) c= rng S ) by Def3, RELAT_1:26;
hence  rng (R * S) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def_3 ::_thesis: verum
end;
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
proof
 ( rng S c= NAT & rng (R * S) c= rng S ) by Def6, RELAT_1:26;
hence  rng (R * S) c= NAT by XBOOLE_1:1; :: according to VALUED_0:def_6 ::_thesis: verum
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
thus  ( f is complex-valued implies for x being set st x in dom f holds
f . x is complex ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is complex ) implies f is complex-valued )
proof
assume A1: f is complex-valued ; ::_thesis: for x being set st x in dom f holds
f . x is complex
let x be set ; ::_thesis: ( x in dom f implies f . x is complex )
assume A2: x in dom f ; ::_thesis: f . x is complex
reconsider f = f as complex-valued Function by A1;
 f . x in rng f by A2, FUNCT_1:3;
hence  f . x is complex ; ::_thesis: verum
end;
assume A3: for x being set st x in dom f holds
f . x is complex ; ::_thesis: f is complex-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_1 ::_thesis: ( not y in rng f or y in COMPLEX )
assume  y in rng f ; ::_thesis: y in COMPLEX
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then  y is complex by A3;
hence  y in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
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
thus  ( f is ext-real-valued implies for x being set st x in dom f holds
f . x is ext-real ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is ext-real ) implies f is ext-real-valued )
proof
assume A4: f is ext-real-valued ; ::_thesis: for x being set st x in dom f holds
f . x is ext-real
let x be set ; ::_thesis: ( x in dom f implies f . x is ext-real )
assume A5: x in dom f ; ::_thesis: f . x is ext-real
reconsider f = f as ext-real-valued Function by A4;
 f . x in rng f by A5, FUNCT_1:3;
hence  f . x is ext-real ; ::_thesis: verum
end;
assume A6: for x being set st x in dom f holds
f . x is ext-real ; ::_thesis: f is ext-real-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_2 ::_thesis: ( not y in rng f or y in ExtREAL )
assume  y in rng f ; ::_thesis: y in ExtREAL
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then  y is ext-real by A6;
hence  y in ExtREAL by XXREAL_0:def_1; ::_thesis: verum
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
thus  ( f is real-valued implies for x being set st x in dom f holds
f . x is real ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is real ) implies f is real-valued )
proof
assume A7: f is real-valued ; ::_thesis: for x being set st x in dom f holds
f . x is real
let x be set ; ::_thesis: ( x in dom f implies f . x is real )
assume A8: x in dom f ; ::_thesis: f . x is real
reconsider f = f as real-valued Function by A7;
 f . x in rng f by A8, FUNCT_1:3;
hence  f . x is real ; ::_thesis: verum
end;
assume A9: for x being set st x in dom f holds
f . x is real ; ::_thesis: f is real-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_3 ::_thesis: ( not y in rng f or y in REAL )
assume  y in rng f ; ::_thesis: y in REAL
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then  y is real by A9;
hence  y in REAL by XREAL_0:def_1; ::_thesis: verum
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
thus  ( f is natural-valued implies for x being set st x in dom f holds
f . x is natural ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is natural ) implies f is natural-valued )
proof
assume A10: f is natural-valued ; ::_thesis: for x being set st x in dom f holds
f . x is natural
let x be set ; ::_thesis: ( x in dom f implies f . x is natural )
assume A11: x in dom f ; ::_thesis: f . x is natural
reconsider f = f as natural-valued Function by A10;
 f . x in rng f by A11, FUNCT_1:3;
hence  f . x is natural ; ::_thesis: verum
end;
assume A12: for x being set st x in dom f holds
f . x is natural ; ::_thesis: f is natural-valued
let y be set ; :: according to TARSKI:def_3,VALUED_0:def_6 ::_thesis: ( not y in rng f or y in NAT )
assume  y in rng f ; ::_thesis: y in NAT
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
then  y is natural by A12;
hence  y in NAT by ORDINAL1:def_12; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is complex-valued iff for x being set holds f . x is complex )
hereby  ::_thesis: ( ( for x being set holds f . x is complex ) implies f is complex-valued )
assume A1: f is complex-valued ; ::_thesis: for x being set holds f . b2 is complex
let x be set ; ::_thesis: f . b1 is complex
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is complex
hence  f . x is complex by A1, Def7; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is complex
hence  f . x is complex by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume  for x being set holds f . x is complex ; ::_thesis: f is complex-valued
then  for x being set st x in dom f holds
f . x is complex ;
hence  f is complex-valued by Def7; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is ext-real-valued iff for x being set holds f . x is ext-real )
hereby  ::_thesis: ( ( for x being set holds f . x is ext-real ) implies f is ext-real-valued )
assume A1: f is ext-real-valued ; ::_thesis: for x being set holds f . b2 is ext-real
let x be set ; ::_thesis: f . b1 is ext-real
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is ext-real
hence  f . x is ext-real by A1, Def8; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is ext-real
hence  f . x is ext-real by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume  for x being set holds f . x is ext-real ; ::_thesis: f is ext-real-valued
then  for x being set st x in dom f holds
f . x is ext-real ;
hence  f is ext-real-valued by Def8; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is real-valued iff for x being set holds f . x is real )
hereby  ::_thesis: ( ( for x being set holds f . x is real ) implies f is real-valued )
assume A1: f is real-valued ; ::_thesis: for x being set holds f . b2 is real
let x be set ; ::_thesis: f . b1 is real
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is real
hence  f . x is real by A1, Def9; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is real
hence  f . x is real by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume  for x being set holds f . x is real ; ::_thesis: f is real-valued
then  for x being set st x in dom f holds
f . x is real ;
hence  f is real-valued by Def9; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is RAT -valued iff for x being set holds f . x is rational )
hereby  ::_thesis: ( ( for x being set holds f . x is rational ) implies f is RAT -valued )
assume A1: f is RAT -valued ; ::_thesis: for x being set holds f . b2 is rational
let x be set ; ::_thesis: f . b1 is rational
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is rational
then  f . x in rng f by FUNCT_1:def_3;
hence  f . x is rational by A1; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is rational
hence  f . x is rational by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for x being set holds f . x is rational ; ::_thesis: f is RAT -valued
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in RAT )
assume  y in rng f ; ::_thesis: y in RAT
then consider x being set  such that
 x in dom f and
A3: f . x = y by FUNCT_1:def_3;
 f . x is rational by A2;
hence  y in RAT by A3, RAT_1:def_2; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is INT -valued iff for x being set holds f . x is integer )
hereby  ::_thesis: ( ( for x being set holds f . x is integer ) implies f is INT -valued )
assume A1: f is INT -valued ; ::_thesis: for x being set holds f . b2 is integer
let x be set ; ::_thesis: f . b1 is integer
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is integer
then  f . x in rng f by FUNCT_1:def_3;
hence  f . x is integer by A1; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is integer
hence  f . x is integer by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume A2: for x being set holds f . x is integer ; ::_thesis: f is INT -valued
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng f or y in INT )
assume  y in rng f ; ::_thesis: y in INT
then consider x being set  such that
 x in dom f and
A3: f . x = y by FUNCT_1:def_3;
 f . x is integer by A2;
hence  y in INT by A3, INT_1:def_2; ::_thesis: verum
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
let f be Function; ::_thesis: ( f is natural-valued iff for x being set holds f . x is natural )
hereby  ::_thesis: ( ( for x being set holds f . x is natural ) implies f is natural-valued )
assume A1: f is natural-valued ; ::_thesis: for x being set holds f . b2 is natural
let x be set ; ::_thesis: f . b1 is natural
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . b1 is natural
hence  f . x is natural by A1, Def12; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . b1 is natural
hence  f . x is natural by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume  for x being set holds f . x is natural ; ::_thesis: f is natural-valued
then  for x being set st x in dom f holds
f . x is natural ;
hence  f is natural-valued by Def12; ::_thesis: verum
end;

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
proof
 rng (X --> x) c= COMPLEX by MEMBERED:1;
hence  X --> x is complex-valued by Def1; ::_thesis: verum
end;
end;

registration
let X be set ;
let x be ext-real number ;
clusterX --> x ->  ext-real-valued ;
coherence
 X --> x is ext-real-valued
proof
 rng (X --> x) c= ExtREAL by MEMBERED:2;
hence  X --> x is ext-real-valued by Def2; ::_thesis: verum
end;
end;

registration
let X be set ;
let x be real number ;
clusterX --> x ->  real-valued ;
coherence
 X --> x is real-valued
proof
 rng (X --> x) c= REAL by MEMBERED:3;
hence  X --> x is real-valued by Def3; ::_thesis: verum
end;
end;

registration
let X be set ;
let x be rational number ;
clusterX --> x ->  RAT -valued ;
coherence
 X --> x is RAT -valued
proof
 rng (X --> x) c= RAT by MEMBERED:4;
hence  X --> x is RAT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let X be set ;
let x be integer number ;
clusterX --> x ->  INT -valued ;
coherence
 X --> x is INT -valued
proof
 rng (X --> x) c= INT by MEMBERED:5;
hence  X --> x is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let X be set ;
let x be Nat;
clusterX --> x ->  natural-valued ;
coherence
 X --> x is natural-valued
proof
 rng (X --> x) c= NAT by MEMBERED:6;
hence  X --> x is natural-valued by Def6; ::_thesis: verum
end;
end;

registration
let f, g be complex-valued Function;
clusterf +* g ->  complex-valued ;
coherence
 f +* g is complex-valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= COMPLEX by MEMBERED:1;
hence  f +* g is complex-valued by Def1; ::_thesis: verum
end;
end;

registration
let f, g be ext-real-valued Function;
clusterf +* g ->  ext-real-valued ;
coherence
 f +* g is ext-real-valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= ExtREAL by MEMBERED:2;
hence  f +* g is ext-real-valued by Def2; ::_thesis: verum
end;
end;

registration
let f, g be real-valued Function;
clusterf +* g ->  real-valued ;
coherence
 f +* g is real-valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= REAL by MEMBERED:3;
hence  f +* g is real-valued by Def3; ::_thesis: verum
end;
end;

registration
let f, g be RAT -valued Function;
clusterf +* g ->  RAT -valued ;
coherence
 f +* g is RAT -valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= RAT by MEMBERED:4;
hence  f +* g is RAT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let f, g be INT -valued Function;
clusterf +* g ->  INT -valued ;
coherence
 f +* g is INT -valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= INT by MEMBERED:5;
hence  f +* g is INT -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let f, g be natural-valued Function;
clusterf +* g ->  natural-valued ;
coherence
 f +* g is natural-valued
proof
 rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then  rng (f +* g) c= NAT by MEMBERED:6;
hence  f +* g is natural-valued by Def6; ::_thesis: verum
end;
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
proof
let R be Relation of X,Y; ::_thesis: R is complex-valued
thus  rng R c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
let R be Relation of X,Y; ::_thesis: R is ext-real-valued
thus  rng R c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
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
let R be Relation of X,Y; ::_thesis: R is real-valued
thus  rng R c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation of X,Y; ::_thesis: R is RAT -valued
thus  rng R c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
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
let R be Relation of X,Y; ::_thesis: R is INT -valued
thus  rng R c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
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
let R be Relation of X,Y; ::_thesis: R is natural-valued
thus  rng R c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= COMPLEX by MEMBERED:1; :: according to VALUED_0:def_1 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= ExtREAL by MEMBERED:2; :: according to VALUED_0:def_2 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= REAL by MEMBERED:3; :: according to VALUED_0:def_3 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= RAT by MEMBERED:4; :: according to RELAT_1:def_19 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= INT by MEMBERED:5; :: according to RELAT_1:def_19 ::_thesis: verum
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
 rng [:X,Y:] c= Y by RELAT_1:159;
hence  rng [:X,Y:] c= NAT by MEMBERED:6; :: according to VALUED_0:def_6 ::_thesis: verum
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
take  1 .--> 1 ; ::_thesis: ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued )
thus  ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued & 1 .--> 1 is INT -valued & 1 .--> 1 is RAT -valued ) ; ::_thesis: verum
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
let f be non empty constant complex-valued Function; ::_thesis: ex r being complex number st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being complex number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty constant ext-real-valued Function; ::_thesis: ex r being ext-real number st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being ext-real number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty constant real-valued Function; ::_thesis: ex r being real number st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being real number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty RAT -valued constant Function; ::_thesis: ex r being rational number st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being rational number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty INT -valued constant Function; ::_thesis: ex r being integer number st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being integer number st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
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
let f be non empty constant natural-valued Function; ::_thesis: ex r being Nat st
for x being set st x in dom f holds
f . x = r
consider r being set  such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:78;
consider x being set  such that
A2: x in dom f by XBOOLE_0:def_1;
 r = f . x by A1, A2;
hence  ex r being Nat st
for x being set st x in dom f holds
f . x = r by A1; ::_thesis: verum
end;

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 & e2 in dom f & 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 & e2 in dom f & 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 & e2 in dom f & 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 & 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 for set ;
coherence
 for b1 being ext-real-valued Function st b1 is trivial holds
( b1 is increasing & b1 is decreasing )
proof
let f be ext-real-valued Function; ::_thesis: ( f is trivial implies ( f is increasing & f is decreasing ) )
assume A1: f is trivial ; ::_thesis: ( f is increasing & f is decreasing )
thus  f is increasing ::_thesis: f is decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 < f . e2 )
assume  ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 < f . e2 )
hence  ( not e1 < e2 or f . e1 < f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 > f . e2 )
assume  ( e1 in dom f & e2 in dom f ) ; ::_thesis: ( not e1 < e2 or f . e1 > f . e2 )
hence  ( not e1 < e2 or f . e1 > f . e2 ) by A1, ZFMISC_1:def_10; ::_thesis: verum
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
let f be ext-real-valued Function; ::_thesis: ( f is increasing implies f is non-decreasing )
assume A1: f is increasing ; ::_thesis: f is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 <= f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 <= f . e2 )
assume that
A2: ( e1 in dom f & e2 in dom f ) and
A3: e1 <= e2 ; ::_thesis: f . e1 <= f . e2
percases ( e1 = e2 or e1 < e2 ) by A3, XXREAL_0:1;
suppose e1 = e2 ; ::_thesis: f . e1 <= f . e2
hence  f . e1 <= f . e2 ; ::_thesis: verum
end;
suppose e1 < e2 ; ::_thesis: f . e1 <= f . e2
hence  f . e1 <= f . e2 by A1, A2, Def13; ::_thesis: verum
end;
end;
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
let f be ext-real-valued Function; ::_thesis: ( f is decreasing implies f is non-increasing )
assume A4: f is decreasing ; ::_thesis: f is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 <= e2 holds
f . e1 >= f . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom f & e2 in dom f & e1 <= e2 implies f . e1 >= f . e2 )
assume that
A5: ( e1 in dom f & e2 in dom f ) and
A6: e1 <= e2 ; ::_thesis: f . e1 >= f . e2
percases ( e1 = e2 or e1 < e2 ) by A6, XXREAL_0:1;
suppose e1 = e2 ; ::_thesis: f . e1 >= f . e2
hence  f . e1 >= f . e2 ; ::_thesis: verum
end;
suppose e1 < e2 ; ::_thesis: f . e1 >= f . e2
hence  f . e1 >= f . e2 by A4, A5, Def14; ::_thesis: verum
end;
end;
end;
end;

registration
let f, g be ext-real-valued increasing Function;
clusterf * g ->  increasing ;
coherence
 g * f is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 < (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2
then A7: f . e1 < f . e2 by A3, A5, Def13;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum
end;
end;

registration
let f, g be ext-real-valued non-decreasing Function;
clusterf * g ->  non-decreasing ;
coherence
 g * f is non-decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2
then A7: f . e1 <= f . e2 by A3, A5, Def15;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum
end;
end;

registration
let f, g be ext-real-valued decreasing Function;
clusterf * g ->  increasing ;
coherence
 g * f is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 < (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 < (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 < (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 < e2 ; ::_thesis: (g * f) . e1 < (g * f) . e2
then A7: f . e1 > f . e2 by A3, A5, Def14;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 < (g * f) . e2 by A4, A6, A7, Def14; ::_thesis: verum
end;
end;

registration
let f, g be ext-real-valued non-increasing Function;
clusterf * g ->  non-decreasing ;
coherence
 g * f is non-decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 <= e2 ; ::_thesis: (g * f) . e1 <= (g * f) . e2
then A7: f . e1 >= f . e2 by A3, A5, Def16;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def16; ::_thesis: verum
end;
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
proof
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 holds
(g * f) . e1 > (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 < e2 implies (g * f) . e1 > (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 < e2 or (g * f) . e1 > (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 < e2 ; ::_thesis: (g * f) . e1 > (g * f) . e2
then A7: f . e1 > f . e2 by A3, A5, Def14;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 > (g * f) . e2 by A4, A6, A7, Def13; ::_thesis: verum
end;
clusterg * f ->  decreasing ;
coherence
 f * g is decreasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 holds
(f * g) . e1 > (f * g) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 implies (f * g) . e1 > (f * g) . e2 )
assume that
A8: e1 in dom (f * g) and
A9: e2 in dom (f * g) ; ::_thesis: ( not e1 < e2 or (f * g) . e1 > (f * g) . e2 )
A10: e1 in dom g by A8, FUNCT_1:11;
then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13;
A12: e2 in dom g by A9, FUNCT_1:11;
then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13;
assume  e1 < e2 ; ::_thesis: (f * g) . e1 > (f * g) . e2
then A14: g . e1 < g . e2 by A10, A12, Def13;
 ( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11;
hence  (f * g) . e1 > (f * g) . e2 by A11, A13, A14, Def14; ::_thesis: verum
end;
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
proof
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 >= (g * f) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 >= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; ::_thesis: ( not e1 <= e2 or (g * f) . e1 >= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume  e1 <= e2 ; ::_thesis: (g * f) . e1 >= (g * f) . e2
then A7: f . e1 >= f . e2 by A3, A5, Def16;
 ( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence  (g * f) . e1 >= (g * f) . e2 by A4, A6, A7, Def15; ::_thesis: verum
end;
clusterg * f ->  non-increasing ;
coherence
 f * g is non-increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for e2 being ext-real number st e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 holds
(f * g) . e1 >= (f * g) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 <= e2 implies (f * g) . e1 >= (f * g) . e2 )
assume that
A8: e1 in dom (f * g) and
A9: e2 in dom (f * g) ; ::_thesis: ( not e1 <= e2 or (f * g) . e1 >= (f * g) . e2 )
A10: e1 in dom g by A8, FUNCT_1:11;
then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13;
A12: e2 in dom g by A9, FUNCT_1:11;
then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13;
assume  e1 <= e2 ; ::_thesis: (f * g) . e1 >= (f * g) . e2
then A14: g . e1 <= g . e2 by A10, A12, Def15;
 ( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11;
hence  (f * g) . e1 >= (f * g) . e2 by A11, A13, A14, Def16; ::_thesis: verum
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
 id X is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom (id X) & e2 in dom (id X) & e1 < e2 holds
(id X) . e1 < (id X) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom (id X) & e2 in dom (id X) & e1 < e2 implies (id X) . e1 < (id X) . e2 )
assume that
A1: e1 in dom (id X) and
A2: e2 in dom (id X) ; ::_thesis: ( not e1 < e2 or (id X) . e1 < (id X) . e2 )
 (id X) . e1 = e1 by A1, FUNCT_1:18;
hence  ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) by A2, FUNCT_1:18; ::_thesis: verum
end;
hence  for b1 being Function of X,X st b1 = id X holds
b1 is increasing ; ::_thesis: verum
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
take  id NAT ; ::_thesis: id NAT is increasing
thus  id NAT is increasing ; ::_thesis: verum
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
take  s ; ::_thesis: ex N being increasing sequence of NAT st s = s * N
take  id NAT ; ::_thesis: s = s * (id NAT)
 dom s = NAT by PARTFUN1:def_2;
hence  s = s * (id NAT) by RELAT_1:52; ::_thesis: verum
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
let x be non empty set ; ::_thesis: for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M
let M be ManySortedSet of NAT ; ::_thesis: for s being subsequence of M holds rng s c= rng M
let s be subsequence of M; ::_thesis: rng s c= rng M
 ex N being increasing sequence of NAT st s = M * N by Def17;
hence  rng s c= rng M by RELAT_1:26; ::_thesis: verum
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
let ss be subsequence of s; ::_thesis: ss is X -valued
 rng ss c= rng s by Lm1;
hence  rng ss c= X by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
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
let ss be subsequence of s; ::_thesis: ss is sequence of X
 ( rng ss c= X & dom ss = NAT ) by PARTFUN1:def_2;
hence  ss is sequence of X by RELSET_1:4; ::_thesis: verum
end;
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
proof
set N = (id NAT) ^\ k;
 (id NAT) ^\ k is increasing
proof
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for e2 being ext-real number st e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 holds
((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2
let e2 be ext-real number ; ::_thesis: ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) & e1 < e2 implies ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 )
assume  ( e1 in dom ((id NAT) ^\ k) & e2 in dom ((id NAT) ^\ k) ) ; ::_thesis: ( not e1 < e2 or ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 )
then reconsider i = e1, j = e2 as Element of NAT ;
A1: ((id NAT) ^\ k) . j = (id NAT) . (j + k) by NAT_1:def_3
.= j + k by FUNCT_1:18 ;
assume A2: e1 < e2 ; ::_thesis: ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2
((id NAT) ^\ k) . i = (id NAT) . (i + k) by NAT_1:def_3
.= i + k by FUNCT_1:18 ;
hence  ((id NAT) ^\ k) . e1 < ((id NAT) ^\ k) . e2 by A1, A2, XREAL_1:6; ::_thesis: verum
end;
then reconsider N = (id NAT) ^\ k as increasing sequence of NAT ;
thus  s ^\ k is subsequence of s ::_thesis: verum
proof
take  N ; :: according to VALUED_0:def_17 ::_thesis: s ^\ k = s * N
thus s ^\ k = (s * (id NAT)) ^\ k by FUNCT_2:17
.= s * N by NAT_1:50 ; ::_thesis: verum
end;
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
let XX be non empty set ; ::_thesis: for ss being sequence of XX holds ss is subsequence of ss
let ss be sequence of XX; ::_thesis: ss is subsequence of ss
take  id NAT ; :: according to VALUED_0:def_17 ::_thesis: ss = ss * (id NAT)
thus  ss = ss * (id NAT) by FUNCT_2:17; ::_thesis: verum
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
let XX be non empty set ; ::_thesis: 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
let ss1, ss2, ss3 be sequence of XX; ::_thesis: ( ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies ss1 is subsequence of ss3 )
given N1 being increasing sequence of NAT such that A1: ss1 = ss2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ( not ss2 is subsequence of ss3 or ss1 is subsequence of ss3 )
given N2 being increasing sequence of NAT such that A2: ss2 = ss3 * N2 ; :: according to VALUED_0:def_17 ::_thesis: ss1 is subsequence of ss3
take  N2 * N1 ; :: according to VALUED_0:def_17 ::_thesis: ss1 = ss3 * (N2 * N1)
thus  ss1 = ss3 * (N2 * N1) by A1, A2, RELAT_1:36; ::_thesis: verum
end;

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
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: ex b1 being sequence of X st b1 is constant
then reconsider s = {} as sequence of X by FUNCT_2:def_1, RELSET_1:12;
take  s ; ::_thesis: s is constant
thus  s is constant ; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ex b1 being sequence of X st b1 is constant
then consider x being set  such that
A1: x in X by XBOOLE_0:def_1;
reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45;
take  s ; ::_thesis: s is constant
thus  s is constant ; ::_thesis: verum
end;
end;
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
let XX be non empty set ; ::_thesis: for ss being sequence of XX
for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss be sequence of XX; ::_thesis: for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss1 be subsequence of ss; ::_thesis: rng ss1 c= rng ss
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ss1 or x in rng ss )
consider N being increasing sequence of NAT such that
A1: ss1 = ss * N by Def17;
assume  x in rng ss1 ; ::_thesis: x in rng ss
then consider n being set  such that
A2: n in NAT and
A3: x = ss1 . n by FUNCT_2:11;
A4: N . n in NAT by A2, FUNCT_2:5;
 x = ss . (N . n) by A1, A2, A3, FUNCT_2:15;
hence  x in rng ss by A4, FUNCT_2:4; ::_thesis: verum
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
let s1 be subsequence of s; ::_thesis: s1 is constant
 rng s1 c= rng s by Th21;
hence  s1 is constant ; ::_thesis: verum
end;
end;

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 & s1 is subsequence of s holds
h /* s1 is subsequence of h /* s
proof
let X, Y be non empty set ; ::_thesis: 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
let s, s1 be sequence of X; ::_thesis: 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
let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h & s1 is subsequence of s implies h /* s1 is subsequence of h /* s )
assume that
A1: rng s c= dom h and
A2: s1 is subsequence of s ; ::_thesis: h /* s1 is subsequence of h /* s
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def17;
take  N ; :: according to VALUED_0:def_17 ::_thesis: h /* s1 = (h /* s) * N
thus  h /* s1 = (h /* s) * N by A1, A3, FUNCT_2:110; ::_thesis: verum
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 for Element of bool [:NAT,X:];
existence
 ex b1 being sequence of X st b1 is non-empty
proof
consider x being non empty set  such that
A1: x in X by SETFAM_1:def_10;
reconsider s = NAT --> x as sequence of X by A1, FUNCOP_1:45;
take  s ; ::_thesis: s is non-empty
thus  s is non-empty ; ::_thesis: verum
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
let s1 be subsequence of s; ::_thesis: s1 is non-empty
 rng s1 c= rng s by Th21;
hence  not {} in rng s1 ; :: according to RELAT_1:def_9 ::_thesis: verum
end;
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 )
proof
hereby  ::_thesis: ( ex x being Element of X st
for n being Nat holds s . n = x implies s is constant )
assume  s is constant ; ::_thesis: ex x being Element of X st
for n being Nat holds s . n = x
then consider x being Element of X such that
A1: for n being Element of NAT st n in dom s holds
s . n = x by PARTFUN2:def_1;
take x = x; ::_thesis: for n being Nat holds s . n = x
let n be Nat; ::_thesis: s . n = x
 ( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence  s . n = x by A1; ::_thesis: verum
end;
given x being Element of X such that A2: for n being Nat holds s . n = x ; ::_thesis: s is constant
take  x ; :: according to PARTFUN2:def_1 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom s or s . b1 = x )
thus  for b1 being Element of NAT holds
( not b1 in dom s or s . b1 = x ) by A2; ::_thesis: verum
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
let i, j be Nat; ::_thesis: for X being set
for s being constant sequence of X holds s . i = s . j
let X be set ; ::_thesis: for s being constant sequence of X holds s . i = s . j
let s be constant sequence of X; ::_thesis: s . i = s . j
percases ( X is empty or not X is empty ) ;
supposeA1: X is empty ; ::_thesis: s . i = s . j
then  s . i = {} ;
hence  s . i = s . j by A1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: s . i = s . j
then  dom s = NAT by FUNCT_2:def_1;
then  ( i in dom s & j in dom s ) by ORDINAL1:def_12;
hence  s . i = s . j by FUNCT_1:def_10; ::_thesis: verum
end;
end;
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
let X be non empty set ; ::_thesis: for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is V29()
let s be sequence of X; ::_thesis: ( ( for i, j being Nat holds s . i = s . j ) implies s is V29() )
assume  for i, j being Nat holds s . i = s . j ; ::_thesis: s is V29()
then  for x, y being set st x in dom s & y in dom s holds
s . x = s . y ;
hence  s is V29() by FUNCT_1:def_10; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is V29()
let s be sequence of X; ::_thesis: ( ( for i being Nat holds s . i = s . (i + 1) ) implies s is V29() )
assume A1: for i being Nat holds s . i = s . (i + 1) ; ::_thesis: s is V29()
now__::_thesis:_for_i,_j_being_Nat_holds_s_._i_=_s_._j
let i, j be Nat; ::_thesis: s . i = s . j
A2: now__::_thesis:_for_i,_j_being_Nat_st_i_<=_j_holds_
s_._i_=_s_._j
let i, j be Nat; ::_thesis: ( i <= j implies s . i = s . j )
assume A3: i <= j ; ::_thesis: s . i = s . j
defpred S1[ Nat] means ( i <= $1 implies s . i = s . $1 );
A4: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A5: S1[j] ; ::_thesis: S1[j + 1]
assume  i <= j + 1 ; ::_thesis: s . i = s . (j + 1)
then  ( i < j + 1 or i = j + 1 ) by XXREAL_0:1;
hence  s . i = s . (j + 1) by A1, A5, NAT_1:13; ::_thesis: verum
end;
A6: S1[ 0 ] by NAT_1:3;
 for j being Nat holds S1[j] from NAT_1:sch_2(A6, A4);
hence  s . i = s . j by A3; ::_thesis: verum
end;
 ( i <= j or j <= i ) ;
hence  s . i = s . j by A2; ::_thesis: verum
end;
hence  s is V29() by Th24; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for s, s1 being sequence of X st s is V29() & s1 is subsequence of s holds
s = s1
let s, s1 be sequence of X; ::_thesis: ( s is V29() & s1 is subsequence of s implies s = s1 )
assume that
A1: s is V29() and
A2: s1 is subsequence of s ; ::_thesis: s = s1
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: s . n = s1 . n
consider N being increasing sequence of NAT such that
A3: s1 = s * N by A2, Def17;
thus s1 . n = s . (N . n) by A3, FUNCT_2:15
.= s . n by A1, Th23 ; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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)
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let h be PartFunc of X,Y; ::_thesis: for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let n be Nat; ::_thesis: ( rng s c= dom h implies (h /* s) ^\ n = h /* (s ^\ n) )
assume A1: rng s c= dom h ; ::_thesis: (h /* s) ^\ n = h /* (s ^\ n)
let m be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((h /* s) ^\ n) . m = (h /* (s ^\ n)) . m
A2: rng (s ^\ n) c= rng s by Th21;
thus ((h /* s) ^\ n) . m = (h /* s) . (m + n) by NAT_1:def_3
.= h . (s . (m + n)) by A1, FUNCT_2:108
.= h . ((s ^\ n) . m) by NAT_1:def_3
.= (h /* (s ^\ n)) . m by A1, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for s being sequence of X
for n being Nat holds s . n in rng s
let s be sequence of X; ::_thesis: for n being Nat holds s . n in rng s
let n be Nat; ::_thesis: s . n in rng s
 n in NAT by ORDINAL1:def_12;
hence  s . n in rng s by FUNCT_2:112; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y
for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let h be PartFunc of X,Y; ::_thesis: for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let n be Nat; ::_thesis: ( h is total implies h /* (s ^\ n) = (h /* s) ^\ n )
assume  h is total ; ::_thesis: h /* (s ^\ n) = (h /* s) ^\ n
then  dom h = X by PARTFUN1:def_2;
then  rng s c= dom h ;
hence  h /* (s ^\ n) = (h /* s) ^\ n by Th27; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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)
let s be sequence of X; ::_thesis: for h being PartFunc of X,Y st rng s c= dom h holds
h .: (rng s) = rng (h /* s)
let h be PartFunc of X,Y; ::_thesis: ( rng s c= dom h implies h .: (rng s) = rng (h /* s) )
assume A1: rng s c= dom h ; ::_thesis: h .: (rng s) = rng (h /* s)
now__::_thesis:_for_r_being_Element_of_Y_holds_
(_(_r_in_h_.:_(rng_s)_implies_r_in_rng_(h_/*_s)_)_&_(_r_in_rng_(h_/*_s)_implies_r_in_h_.:_(rng_s)_)_)
let r be Element of Y; ::_thesis: ( ( r in h .: (rng s) implies r in rng (h /* s) ) & ( r in rng (h /* s) implies r in h .: (rng s) ) )
thus  ( r in h .: (rng s) implies r in rng (h /* s) ) ::_thesis: ( r in rng (h /* s) implies r in h .: (rng s) )
proof
assume  r in h .: (rng s) ; ::_thesis: r in rng (h /* s)
then consider p being Element of X such that
 p in dom h and
A2: p in rng s and
A3: r = h . p by PARTFUN2:59;
consider n being Element of NAT  such that
A4: p = s . n by A2, FUNCT_2:113;
 r = (h /* s) . n by A1, A3, A4, FUNCT_2:108;
hence  r in rng (h /* s) by Th28; ::_thesis: verum
end;
assume  r in rng (h /* s) ; ::_thesis: r in h .: (rng s)
then consider n being Element of NAT  such that
A5: (h /* s) . n = r by FUNCT_2:113;
A6: s . n in rng s by Th28;
 r = h . (s . n) by A1, A5, FUNCT_2:108;
hence  r in h .: (rng s) by A1, A6, FUNCT_1:def_6; ::_thesis: verum
end;
hence  h .: (rng s) = rng (h /* s) by SUBSET_1:3; ::_thesis: verum
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
let X, Y be non empty set ; ::_thesis: 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
let Z be set ; ::_thesis: 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
let s be sequence of X; ::_thesis: 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
let h1 be PartFunc of X,Y; ::_thesis: for h2 being PartFunc of Y,Z st rng s c= dom (h2 * h1) holds
h2 /* (h1 /* s) = (h2 * h1) /* s
let h2 be PartFunc of Y,Z; ::_thesis: ( rng s c= dom (h2 * h1) implies h2 /* (h1 /* s) = (h2 * h1) /* s )
assume A1: rng s c= dom (h2 * h1) ; ::_thesis: h2 /* (h1 /* s) = (h2 * h1) /* s
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h2_*_h1)_/*_s)_._n_=_(h2_/*_(h1_/*_s))_._n
let n be Element of NAT ; ::_thesis: ((h2 * h1) /* s) . n = (h2 /* (h1 /* s)) . n
A2: rng s c= dom h1 by A1, FUNCT_1:101;
 h1 .: (rng s) c= dom h2 by A1, FUNCT_1:101;
then A3: rng (h1 /* s) c= dom h2 by A2, Th30;
 s . n in rng s by Th28;
then A4: s . n in dom h1 by A1, FUNCT_1:11;
thus ((h2 * h1) /* s) . n = (h2 * h1) . (s . n) by A1, FUNCT_2:108
.= h2 . (h1 . (s . n)) by A4, FUNCT_1:13
.= h2 . ((h1 /* s) . n) by A2, FUNCT_2:108
.= (h2 /* (h1 /* s)) . n by A3, FUNCT_2:108 ; ::_thesis: verum
end;
hence  h2 /* (h1 /* s) = (h2 * h1) /* s by FUNCT_2:63; ::_thesis: verum
end;

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

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
let R be Relation; ::_thesis: ( R is COMPLEX -valued implies R is complex-valued )
assume  R is COMPLEX -valued ; ::_thesis: R is complex-valued
hence  rng R c= COMPLEX by RELAT_1:def_19; :: according to VALUED_0:def_1 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is ExtREAL -valued implies R is ext-real-valued )
assume  R is ExtREAL -valued ; ::_thesis: R is ext-real-valued
hence  rng R c= ExtREAL by RELAT_1:def_19; :: according to VALUED_0:def_2 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is REAL -valued implies R is real-valued )
assume  R is REAL -valued ; ::_thesis: R is real-valued
hence  rng R c= REAL by RELAT_1:def_19; :: according to VALUED_0:def_3 ::_thesis: verum
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
let R be Relation; ::_thesis: ( R is NAT -valued implies R is natural-valued )
assume  R is NAT -valued ; ::_thesis: R is natural-valued
hence  rng R c= NAT by RELAT_1:def_19; :: according to VALUED_0:def_6 ::_thesis: verum
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
A1: dom s = NAT by PARTFUN1:def_2;
hereby  ::_thesis: ( ex x being set st
for n being Nat holds s . n = x implies s is constant )
assume A2: s is constant ; ::_thesis: ex x being set st
for n being Nat holds s . n = x
take x = s . 0; ::_thesis: for n being Nat holds s . n = x
let n be Nat; ::_thesis: s . n = x
 ( 0 in dom s & n in dom s ) by A1, ORDINAL1:def_12;
hence  s . n = x by A2, FUNCT_1:def_10; ::_thesis: verum
end;
given x being set  such that A3: for n being Nat holds s . n = x ; ::_thesis: s is constant
let n1, n2 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not n1 in dom s or not n2 in dom s or s . n1 = s . n2 )
assume A4: ( n1 in dom s & n2 in dom s ) ; ::_thesis: s . n1 = s . n2
hence s . n1 = x by A3
.= s . n2 by A3, A4 ;
::_thesis: verum
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
take  X --> 0 ; ::_thesis: X --> 0 is natural-valued
thus  X --> 0 is natural-valued ; ::_thesis: verum
end;
end;