:: Number-Valued Functions
:: by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, MEMBERED, SUBSET_1,
XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, FUNCOP_1, FUNCT_4,
ZFMISC_1, ORDINAL2, ARYTM_3, NAT_1, PARTFUN1, FUNCT_2, SETFAM_1, CARD_1,
VALUED_0, PBOOLE, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
ORDINAL1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4,
NUMBERS, MEMBERED, XCMPLX_0, XREAL_0, XXREAL_0, RAT_1, NAT_1, INT_1;
constructors XCMPLX_0, RAT_1, MEMBERED, FUNCOP_1, FUNCT_4, XXREAL_0, PARTFUN1,
NAT_1, SETFAM_1, RELSET_1, NUMBERS;
registrations MEMBERED, RELAT_1, FUNCOP_1, XREAL_0, RAT_1, ORDINAL1, INT_1,
FUNCT_1, XBOOLE_0, RELSET_1, FUNCT_2, SETFAM_1, SUBSET_1, PBOOLE, NAT_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI, FUNCT_1, RELAT_1, PARTFUN2, FUNCT_2;
equalities XBOOLE_0, FUNCOP_1, RELAT_1;
expansions TARSKI, FUNCT_1, RELAT_1, PARTFUN2, FUNCT_2;
theorems NUMBERS, XBOOLE_1, RELAT_1, MEMBERED, FUNCT_1, XCMPLX_0, XXREAL_0,
XREAL_0, RAT_1, INT_1, ORDINAL1, FUNCT_4, FUNCOP_1, XBOOLE_0, ZFMISC_1,
FUNCT_2, NAT_1, XREAL_1, RELSET_1, SETFAM_1, PARTFUN2, PARTFUN1,
SUBSET_1;
schemes NAT_1;
begin
definition
let f be Relation;
attr f is complex-valued means
:Def1:
rng f c= COMPLEX;
attr f is ext-real-valued means
:Def2:
rng f c= ExtREAL;
attr f is real-valued means
:Def3:
rng f c= REAL;
::$CD 2
attr f is natural-valued means
:Def4:
rng f c= NAT;
end;
registration
cluster natural-valued -> INT-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= NAT;
hence rng R c= INT by NUMBERS:17;
end;
cluster INT-valued -> RAT-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= INT;
hence rng R c= RAT by NUMBERS:14;
end;
cluster INT-valued -> real-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= INT;
hence rng R c= REAL by NUMBERS:15;
end;
cluster RAT-valued -> real-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= RAT;
hence rng R c= REAL by NUMBERS:12;
end;
cluster real-valued -> ext-real-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= REAL;
hence rng R c= ExtREAL by NUMBERS:31;
end;
cluster real-valued -> complex-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= REAL;
hence rng R c= COMPLEX by NUMBERS:11;
end;
cluster natural-valued -> RAT-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= NAT;
hence rng R c= RAT by NUMBERS:18;
end;
cluster natural-valued -> real-valued for Relation;
coherence
proof
let R be Relation;
assume rng R c= NAT;
hence rng R c= REAL by NUMBERS:19;
end;
end;
registration
cluster empty -> natural-valued for Relation;
coherence
proof
let R be Relation;
assume R is empty;
hence rng R c= NAT;
end;
end;
registration
cluster natural-valued for Function;
existence
proof
take {};
thus thesis;
end;
end;
registration
let R be complex-valued Relation;
cluster rng R -> complex-membered;
coherence
proof
rng R c= COMPLEX by Def1;
hence thesis;
end;
end;
registration
let R be ext-real-valued Relation;
cluster rng R -> ext-real-membered;
coherence
proof
rng R c= ExtREAL by Def2;
hence thesis;
end;
end;
registration
let R be real-valued Relation;
cluster rng R -> real-membered;
coherence
proof
rng R c= REAL by Def3;
hence thesis;
end;
end;
registration
let R be RAT-valued Relation;
cluster rng R -> rational-membered;
coherence;
end;
registration
let R be INT-valued Relation;
cluster rng R -> integer-membered;
coherence;
end;
registration
let R be natural-valued Relation;
cluster rng R -> natural-membered;
coherence
proof
rng R c= NAT by Def4;
hence thesis;
end;
end;
reserve x,y for object,X for set,
f for Function,
R,S for Relation;
theorem Th1:
for S being complex-valued Relation st R c= S holds R is complex-valued
proof
let S be complex-valued Relation;
assume R c= S;
then
A1: rng R c= rng S by RELAT_1:11;
rng S c= COMPLEX by Def1;
hence rng R c= COMPLEX by A1;
end;
theorem Th2:
for S being ext-real-valued Relation st R c= S holds R is ext-real-valued
proof
let S be ext-real-valued Relation;
assume R c= S;
then
A1: rng R c= rng S by RELAT_1:11;
rng S c= ExtREAL by Def2;
hence rng R c= ExtREAL by A1;
end;
theorem Th3:
for S being real-valued Relation st R c= S holds R is real-valued
proof
let S be real-valued Relation;
assume R c= S;
then
A1: rng R c= rng S by RELAT_1:11;
rng S c= REAL by Def3;
hence rng R c= REAL by A1;
end;
theorem
for S being RAT-valued Relation st R c= S holds R is RAT-valued;
theorem
for S being INT-valued Relation st R c= S holds R is INT-valued;
theorem Th6:
for S being natural-valued Relation st R c= S holds R is natural-valued
proof
let S be natural-valued Relation;
assume R c= S;
then
A1: rng R c= rng S by RELAT_1:11;
rng S c= NAT by Def4;
hence rng R c= NAT by A1;
end;
registration
let R be complex-valued Relation;
cluster -> complex-valued for Subset of R;
coherence by Th1;
end;
registration
let R be ext-real-valued Relation;
cluster -> ext-real-valued for Subset of R;
coherence by Th2;
end;
registration
let R be real-valued Relation;
cluster -> real-valued for Subset of R;
coherence by Th3;
end;
registration
let R be RAT-valued Relation;
cluster -> RAT-valued for Subset of R;
coherence;
end;
registration
let R be INT-valued Relation;
cluster -> INT-valued for Subset of R;
coherence;
end;
registration
let R be natural-valued Relation;
cluster -> natural-valued for Subset of R;
coherence by Th6;
end;
registration
let R,S be complex-valued Relation;
cluster R \/ S -> complex-valued;
coherence
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;
end;
end;
registration
let R,S be ext-real-valued Relation;
cluster R \/ S -> ext-real-valued;
coherence
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;
end;
end;
registration
let R,S be real-valued Relation;
cluster R \/ S -> real-valued;
coherence
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;
end;
end;
registration
let R,S be RAT-valued Relation;
cluster R \/ S -> RAT-valued;
coherence;
end;
registration
let R,S be INT-valued Relation;
cluster R \/ S -> INT-valued;
coherence;
end;
registration
let R,S be natural-valued Relation;
cluster R \/ S -> natural-valued;
coherence
proof
A1: rng(R \/ S) = rng R \/ rng S by RELAT_1:12;
rng R c= NAT & rng S c= NAT by Def4;
hence rng(R \/ S) c= NAT by A1,XBOOLE_1:8;
end;
end;
registration
let R be complex-valued Relation;
let S;
cluster R /\ S -> complex-valued;
coherence
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;
end;
cluster R \ S -> complex-valued;
coherence;
end;
registration
let R be ext-real-valued Relation;
let S;
cluster R /\ S -> ext-real-valued;
coherence
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;
end;
cluster R \ S -> ext-real-valued;
coherence;
end;
registration
let R be real-valued Relation;
let S;
cluster R /\ S -> real-valued;
coherence
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;
end;
cluster R \ S -> real-valued;
coherence;
end;
registration
let R be RAT-valued Relation;
let S;
cluster R /\ S -> RAT-valued;
coherence;
cluster R \ S -> RAT-valued;
coherence;
end;
registration
let R be INT-valued Relation;
let S;
cluster R /\ S -> INT-valued;
coherence;
cluster R \ S -> INT-valued;
coherence;
end;
registration
let R be natural-valued Relation;
let S;
cluster R /\ S -> natural-valued;
coherence
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 Def4;
hence rng(R /\ S) c= NAT by A1;
end;
cluster R \ S -> natural-valued;
coherence;
end;
registration
let R,S be complex-valued Relation;
cluster R \+\ S -> complex-valued;
coherence;
end;
registration
let R,S be ext-real-valued Relation;
cluster R \+\ S -> ext-real-valued;
coherence;
end;
registration
let R,S be real-valued Relation;
cluster R \+\ S -> real-valued;
coherence;
end;
registration
let R,S be RAT-valued Relation;
cluster R \+\ S -> RAT-valued;
coherence;
end;
registration
let R,S be INT-valued Relation;
cluster R \+\ S -> INT-valued;
coherence;
end;
registration
let R,S be natural-valued Relation;
cluster R \+\ S -> natural-valued;
coherence;
end;
registration
let R be complex-valued Relation;
let X;
cluster R.:X -> complex-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be ext-real-valued Relation;
let X;
cluster R.:X -> ext-real-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be real-valued Relation;
let X;
cluster R.:X -> real-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be RAT-valued Relation;
let X;
cluster R.:X -> rational-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be INT-valued Relation;
let X;
cluster R.:X -> integer-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be natural-valued Relation;
let X;
cluster R.:X -> natural-membered;
coherence
proof
R.:X c= rng R by RELAT_1:111;
hence thesis;
end;
end;
registration
let R be complex-valued Relation;
let x;
cluster Im(R,x) -> complex-membered;
coherence;
end;
registration
let R be ext-real-valued Relation;
let x;
cluster Im(R,x) -> ext-real-membered;
coherence;
end;
registration
let R be real-valued Relation;
let x;
cluster Im(R,x) -> real-membered;
coherence;
end;
registration
let R be RAT-valued Relation;
let x;
cluster Im(R,x) -> rational-membered;
coherence;
end;
registration
let R be INT-valued Relation;
let x;
cluster Im(R,x) -> integer-membered;
coherence;
end;
registration
let R be natural-valued Relation;
let x;
cluster Im(R,x) -> natural-membered;
coherence;
end;
registration
let R be complex-valued Relation;
let X;
cluster R|X -> complex-valued;
coherence
proof
rng R c= COMPLEX & rng(R|X) c= rng R by Def1,RELAT_1:70;
hence rng(R|X) c= COMPLEX;
end;
end;
registration
let R be ext-real-valued Relation;
let X;
cluster R|X -> ext-real-valued;
coherence
proof
rng R c= ExtREAL & rng(R|X) c= rng R by Def2,RELAT_1:70;
hence rng(R|X) c= ExtREAL;
end;
end;
registration
let R be real-valued Relation;
let X;
cluster R|X -> real-valued;
coherence
proof
rng R c= REAL & rng(R|X) c= rng R by Def3,RELAT_1:70;
hence rng(R|X) c= REAL;
end;
end;
registration
let R be RAT-valued Relation;
let X;
cluster R|X -> RAT-valued;
coherence;
end;
registration
let R be INT-valued Relation;
let X;
cluster R|X -> INT-valued;
coherence;
end;
registration
let R be natural-valued Relation;
let X;
cluster R|X -> natural-valued;
coherence
proof
rng R c= NAT & rng(R|X) c= rng R by Def4,RELAT_1:70;
hence rng(R|X) c= NAT;
end;
end;
registration
let X be complex-membered set;
cluster id X -> complex-valued;
coherence
by MEMBERED:1;
end;
registration
let X be ext-real-membered set;
cluster id X -> ext-real-valued;
coherence
by MEMBERED:2;
end;
registration
let X be real-membered set;
cluster id X -> real-valued;
coherence
by MEMBERED:3;
end;
registration
let X be rational-membered set;
cluster id X -> RAT-valued;
coherence
by MEMBERED:4;
end;
registration
let X be integer-membered set;
cluster id X -> INT-valued;
coherence
by MEMBERED:5;
end;
registration
let X be natural-membered set;
cluster id X -> natural-valued;
coherence
by MEMBERED:6;
end;
registration
let R;
let S be complex-valued Relation;
cluster R*S -> complex-valued;
coherence
proof
rng S c= COMPLEX & rng(R*S) c= rng S by Def1,RELAT_1:26;
hence rng(R*S) c= COMPLEX;
end;
end;
registration
let R;
let S be ext-real-valued Relation;
cluster R*S -> ext-real-valued;
coherence
proof
rng S c= ExtREAL & rng(R*S) c= rng S by Def2,RELAT_1:26;
hence rng(R*S) c= ExtREAL;
end;
end;
registration
let R;
let S be real-valued Relation;
cluster R*S -> real-valued;
coherence
proof
rng S c= REAL & rng(R*S) c= rng S by Def3,RELAT_1:26;
hence rng(R*S) c= REAL;
end;
end;
registration
let R;
let S be RAT-valued Relation;
cluster R*S -> RAT-valued;
coherence;
end;
registration
let R;
let S be INT-valued Relation;
cluster R*S -> INT-valued;
coherence;
end;
registration
let R;
let S be natural-valued Relation;
cluster R*S -> natural-valued;
coherence
proof
rng S c= NAT & rng(R*S) c= rng S by Def4,RELAT_1:26;
hence rng(R*S) c= NAT;
end;
end;
definition
let f be Function;
redefine attr f is complex-valued means
for x st x in dom f holds f.x is complex;
compatibility
proof
thus f is complex-valued implies for x st x in dom f holds f.x is complex
proof
assume
A1: f is complex-valued;
let x;
assume
A2: x in dom f;
reconsider f as complex-valued Function by A1;
f.x in rng f by A2,FUNCT_1:3;
hence thesis;
end;
assume
A3: for x st x in dom f holds f.x is complex;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
then y is complex by A3;
hence thesis by XCMPLX_0:def 2;
end;
redefine attr f is ext-real-valued means
for x st x in dom f holds f.x is ext-real;
compatibility
proof
thus f is ext-real-valued implies for x st x in dom f holds f.x is ext-real
proof
assume
A4: f is ext-real-valued;
let x;
assume
A5: x in dom f;
reconsider f as ext-real-valued Function by A4;
f.x in rng f by A5,FUNCT_1:3;
hence thesis;
end;
assume
A6: for x st x in dom f holds f.x is ext-real;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
then y is ext-real by A6;
hence thesis by XXREAL_0:def 1;
end;
redefine attr f is real-valued means
for x st x in dom f holds f.x is real;
compatibility
proof
thus f is real-valued implies for x st x in dom f holds f.x is real
proof
assume
A7: f is real-valued;
let x;
assume
A8: x in dom f;
reconsider f as real-valued Function by A7;
f.x in rng f by A8,FUNCT_1:3;
hence thesis;
end;
assume
A9: for x st x in dom f holds f.x is real;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
then y is real by A9;
hence thesis by XREAL_0:def 1;
end;
::$CD 2
redefine attr f is natural-valued means
for x st x in dom f holds f.x is natural;
compatibility
proof
thus f is natural-valued implies for x st x in dom f holds f.x is natural
proof
assume
A10: f is natural-valued;
let x;
assume
A11: x in dom f;
reconsider f as natural-valued Function by A10;
f.x in rng f by A11,FUNCT_1:3;
hence thesis;
end;
assume
A12: for x st x in dom f holds f.x is natural;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
then y is natural by A12;
hence thesis by ORDINAL1:def 12;
end;
end;
theorem Th7:
f is complex-valued iff for x holds f.x is complex
proof
hereby
assume
A1: f is complex-valued;
let x;
per cases;
suppose
x in dom f;
hence f.x is complex by A1;
end;
suppose
not x in dom f;
hence f.x is complex by FUNCT_1:def 2;
end;
end;
assume for x holds f.x is complex;
then for x st x in dom f holds f.x is complex;
hence thesis;
end;
theorem Th8:
f is ext-real-valued iff for x holds f.x is ext-real
proof
hereby
assume
A1: f is ext-real-valued;
let x;
per cases;
suppose
x in dom f;
hence f.x is ext-real by A1;
end;
suppose
not x in dom f;
hence f.x is ext-real by FUNCT_1:def 2;
end;
end;
assume for x holds f.x is ext-real;
then for x st x in dom f holds f.x is ext-real;
hence thesis;
end;
theorem Th9:
f is real-valued iff for x holds f.x is real
proof
hereby
assume
A1: f is real-valued;
let x;
per cases;
suppose
x in dom f;
hence f.x is real by A1;
end;
suppose
not x in dom f;
hence f.x is real by FUNCT_1:def 2;
end;
end;
assume for x holds f.x is real;
then for x st x in dom f holds f.x is real;
hence thesis;
end;
theorem Th10:
f is RAT-valued iff for x holds f.x is rational
proof
hereby
assume
A1: f is RAT-valued;
let x;
per cases;
suppose x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence f.x is rational by A1;
end;
suppose not x in dom f;
hence f.x is rational by FUNCT_1:def 2;
end;
end;
assume
A2: for x holds f.x is rational;
let y be object;
assume y in rng f;
then consider x being object such that x in dom f and
A3: f.x = y by FUNCT_1:def 3;
f.x is rational by A2;
hence thesis by A3,RAT_1:def 2;
end;
theorem Th11:
f is INT-valued iff for x holds f.x is integer
proof
hereby
assume
A1: f is INT-valued;
let x;
per cases;
suppose x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence f.x is integer by A1;
end;
suppose not x in dom f;
hence f.x is integer by FUNCT_1:def 2;
end;
end;
assume
A2: for x holds f.x is integer;
let y be object;
assume y in rng f;
then consider x being object such that x in dom f and
A3: f.x = y by FUNCT_1:def 3;
f.x is integer by A2;
hence thesis by A3,INT_1:def 2;
end;
theorem Th12:
f is natural-valued iff for x holds f.x is natural
proof
hereby
assume
A1: f is natural-valued;
let x;
per cases;
suppose
x in dom f;
hence f.x is natural by A1;
end;
suppose
not x in dom f;
hence f.x is natural by FUNCT_1:def 2;
end;
end;
assume for x holds f.x is natural;
then for x st x in dom f holds f.x is natural;
hence thesis;
end;
registration
let f be complex-valued Function;
let x be object;
cluster f.x -> complex;
coherence by Th7;
end;
registration
let f be ext-real-valued Function;
let x be object;
cluster f.x -> ext-real;
coherence by Th8;
end;
registration
let f be real-valued Function;
let x be object;
cluster f.x -> real;
coherence by Th9;
end;
registration
let f be RAT-valued Function;
let x be object;
cluster f.x -> rational;
coherence by Th10;
end;
registration
let f be INT-valued Function;
let x be object;
cluster f.x -> integer;
coherence by Th11;
end;
registration
let f be natural-valued Function;
let x be object;
cluster f.x -> natural;
coherence by Th12;
end;
registration
let X;
let x be Complex;
cluster X --> x -> complex-valued;
coherence
proof
rng(X --> x) c= COMPLEX by MEMBERED:1;
hence thesis;
end;
end;
registration
let X;
let x be ExtReal;
cluster X --> x -> ext-real-valued;
coherence
proof
rng(X --> x) c= ExtREAL by MEMBERED:2;
hence thesis;
end;
end;
registration
let X;
let x be Real;
cluster X --> x -> real-valued;
coherence
proof
rng(X --> x) c= REAL by MEMBERED:3;
hence thesis;
end;
end;
registration
let X;
let x be Rational;
cluster X --> x -> RAT-valued;
coherence
proof
rng(X --> x) c= RAT by MEMBERED:4;
hence thesis;
end;
end;
registration
let X;
let x be Integer;
cluster X --> x -> INT-valued;
coherence
proof
rng(X --> x) c= INT by MEMBERED:5;
hence thesis;
end;
end;
registration
let X;
let x be Nat;
cluster X --> x -> natural-valued;
coherence
proof
rng(X --> x) c= NAT by MEMBERED:6;
hence thesis;
end;
end;
registration
let f,g be complex-valued Function;
cluster f +* g -> complex-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= COMPLEX by MEMBERED:1;
hence thesis;
end;
end;
registration
let f,g be ext-real-valued Function;
cluster f +* g -> ext-real-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= ExtREAL by MEMBERED:2;
hence thesis;
end;
end;
registration
let f,g be real-valued Function;
cluster f +* g -> real-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= REAL by MEMBERED:3;
hence thesis;
end;
end;
registration
let f,g be RAT-valued Function;
cluster f +* g -> RAT-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= RAT by MEMBERED:4;
hence thesis;
end;
end;
registration
let f,g be INT-valued Function;
cluster f +* g -> INT-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= INT by MEMBERED:5;
hence thesis;
end;
end;
registration
let f,g be natural-valued Function;
cluster f +* g -> natural-valued;
coherence
proof
rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
then rng(f +* g) c= NAT by MEMBERED:6;
hence thesis;
end;
end;
registration
let x;
let y be Complex;
cluster x .--> y -> complex-valued;
coherence;
end;
registration
let x;
let y be ExtReal;
cluster x .--> y -> ext-real-valued;
coherence;
end;
registration
let x;
let y be Real;
cluster x .--> y -> real-valued;
coherence;
end;
registration
let x;
let y be Rational;
cluster x .--> y -> RAT-valued;
coherence;
end;
registration
let x;
let y be Integer;
cluster x .--> y -> INT-valued;
coherence;
end;
registration
let x;
let y be Nat;
cluster x .--> y -> natural-valued;
coherence;
end;
registration
let X;
let Y be complex-membered set;
cluster -> complex-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= COMPLEX by MEMBERED:1;
end;
end;
registration
let X;
let Y be ext-real-membered set;
cluster -> ext-real-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= ExtREAL by MEMBERED:2;
end;
end;
registration
let X;
let Y be real-membered set;
cluster -> real-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= REAL by MEMBERED:3;
end;
end;
registration
let X;
let Y be rational-membered set;
cluster -> RAT-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= RAT by MEMBERED:4;
end;
end;
registration
let X;
let Y be integer-membered set;
cluster -> INT-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= INT by MEMBERED:5;
end;
end;
registration
let X;
let Y be natural-membered set;
cluster -> natural-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus rng R c= NAT by MEMBERED:6;
end;
end;
registration
let X;
let Y be complex-membered set;
cluster [:X,Y:] -> complex-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= COMPLEX by MEMBERED:1;
end;
end;
registration
let X;
let Y be ext-real-membered set;
cluster [:X,Y:] -> ext-real-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= ExtREAL by MEMBERED:2;
end;
end;
registration
let X;
let Y be real-membered set;
cluster [:X,Y:] -> real-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= REAL by MEMBERED:3;
end;
end;
registration
let X;
let Y be rational-membered set;
cluster [:X,Y:] -> RAT-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= RAT by MEMBERED:4;
end;
end;
registration
let X;
let Y be integer-membered set;
cluster [:X,Y:] -> INT-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= INT by MEMBERED:5;
end;
end;
registration
let X;
let Y be natural-membered set;
cluster [:X,Y:] -> natural-valued;
coherence
proof
rng [:X,Y:] c= Y by RELAT_1:159;
hence rng [:X,Y:] c= NAT by MEMBERED:6;
end;
end;
:::notation
::: synonym f is non-zero for f is non-empty;
:::end;
registration
cluster non empty constant natural-valued INT-valued RAT-valued for Function;
existence
proof
take 1 .--> 1;
thus thesis;
end;
end;
theorem
for f being non empty constant complex-valued Function ex r being
Complex st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant complex-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
theorem
for f being non empty constant ext-real-valued Function ex r being
ExtReal st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant ext-real-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
theorem
for f being non empty constant real-valued Function ex r being Real
st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant real-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
theorem
for f being non empty constant RAT-valued Function ex r being
Rational st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant RAT-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
theorem
for f being non empty constant INT-valued Function ex r being
Integer st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant INT-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
theorem
for f being non empty constant natural-valued Function ex r being
Nat st for x being object st x in dom f holds f.x = r
proof
let f be non empty constant natural-valued Function;
consider r being object such that
A1: for x being object st x in dom f holds f.x = r by FUNCOP_1:78;
consider x being object such that
A2: x in dom f by XBOOLE_0:def 1;
r = f.x by A1,A2;
hence thesis by A1;
end;
begin :: inecreasing & decreasing functions
reserve e1,e2 for ExtReal;
definition
let f be ext-real-valued Function;
attr f is increasing means
:Def9:
for e1,e2 st e1 in dom f & e2 in dom f & e1 < e2 holds f.e1 < f.e2;
attr f is decreasing means
:Def10:
for e1,e2 st e1 in dom f & e2 in dom f & e1 < e2 holds f.e1 > f.e2;
attr f is non-decreasing means
:Def11:
for e1,e2 st e1 in dom f & e2 in dom f & e1 <= e2 holds f.e1 <= f.e2;
attr f is non-increasing means
:Def12:
for e1,e2 st e1 in dom f & e2 in dom f & e1 <= e2 holds f.e1 >= f.e2;
end;
:: 2008.08.31, A.T.
registration
cluster trivial -> increasing decreasing for ext-real-valued Function;
coherence
by ZFMISC_1:def 10;
end;
registration
cluster increasing -> non-decreasing for ext-real-valued Function;
coherence
proof
let f be ext-real-valued Function;
assume
A1: f is increasing;
let e1,e2 such that
A2: e1 in dom f & e2 in dom f and
A3: e1 <= e2;
per cases by A3,XXREAL_0:1;
suppose
e1 = e2;
hence thesis;
end;
suppose
e1 < e2;
hence thesis by A1,A2;
end;
end;
cluster decreasing -> non-increasing for ext-real-valued Function;
coherence
proof
let f be ext-real-valued Function;
assume
A4: f is decreasing;
let e1,e2 such that
A5: e1 in dom f & e2 in dom f and
A6: e1 <= e2;
per cases by A6,XXREAL_0:1;
suppose
e1 = e2;
hence thesis;
end;
suppose
e1 < e2;
hence thesis by A4,A5;
end;
end;
end;
registration
let f,g be increasing ext-real-valued Function;
cluster g*f -> increasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 < f.e2 by A3,A5,Def9;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def9;
end;
end;
registration
let f,g be non-decreasing ext-real-valued Function;
cluster g*f -> non-decreasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 <= f.e2 by A3,A5,Def11;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def11;
end;
end;
registration
let f,g be decreasing ext-real-valued Function;
cluster g*f -> increasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 > f.e2 by A3,A5,Def10;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def10;
end;
end;
registration
let f,g be non-increasing ext-real-valued Function;
cluster g*f -> non-decreasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 >= f.e2 by A3,A5,Def12;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def12;
end;
end;
registration
let f be decreasing ext-real-valued Function;
let g be increasing ext-real-valued Function;
cluster g*f -> decreasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 > f.e2 by A3,A5,Def10;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def9;
end;
cluster f*g -> decreasing;
coherence
proof
let e1,e2;
assume that
A8: e1 in dom(f*g) and
A9: e2 in dom (f*g);
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;
then
A14: g.e1 < g.e2 by A10,A12,Def9;
g.e1 in dom f & g.e2 in dom f by A8,A9,FUNCT_1:11;
hence thesis by A11,A13,A14,Def10;
end;
end;
registration
let f be non-increasing ext-real-valued Function;
let g be non-decreasing ext-real-valued Function;
cluster g*f -> non-increasing;
coherence
proof
let e1,e2;
assume that
A1: e1 in dom(g*f) and
A2: e2 in dom (g*f);
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;
then
A7: f.e1 >= f.e2 by A3,A5,Def12;
f.e1 in dom g & f.e2 in dom g by A1,A2,FUNCT_1:11;
hence thesis by A4,A6,A7,Def11;
end;
cluster f*g -> non-increasing;
coherence
proof
let e1,e2;
assume that
A8: e1 in dom(f*g) and
A9: e2 in dom (f*g);
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;
then
A14: g.e1 <= g.e2 by A10,A12,Def11;
g.e1 in dom f & g.e2 in dom f by A8,A9,FUNCT_1:11;
hence thesis by A11,A13,A14,Def12;
end;
end;
registration
let X be ext-real-membered set;
cluster id X -> increasing for Function of X,X;
coherence
proof
id X is increasing
proof
let e1,e2;
assume that
A1: e1 in dom id X and
A2: e2 in dom id X;
(id X).e1 = e1 by A1,FUNCT_1:18;
hence thesis by A2,FUNCT_1:18;
end;
hence thesis;
end;
end;
registration
cluster increasing for sequence of NAT;
existence
proof
take id NAT;
thus thesis;
end;
end;
definition
let s be ManySortedSet of NAT;
mode subsequence of s -> ManySortedSet of NAT means
:Def13:
ex N being increasing sequence of NAT st it = s * N;
existence
proof
take s,id NAT;
dom s = NAT by PARTFUN1:def 2;
hence thesis by RELAT_1:52;
end;
end;
Lm1:
for x being non empty set, M be ManySortedSet of NAT,
s be subsequence of M
holds rng s c= rng M
proof let x be non empty set, M be ManySortedSet of NAT,
s be subsequence of M;
ex N being increasing sequence of NAT st s = M * N by Def13;
hence rng s c= rng M by RELAT_1:26;
end;
registration
let X be non empty set, s be X-valued ManySortedSet of NAT;
cluster -> X-valued for subsequence of s;
coherence
proof let ss be subsequence of s;
rng ss c= rng s by Lm1;
hence rng ss c= X by XBOOLE_1:1;
end;
end;
definition
let X be non empty set, s be sequence of X;
redefine mode subsequence of s -> sequence of X;
coherence
proof let ss be subsequence of s;
rng ss c= X & dom ss = NAT by PARTFUN1:def 2;
hence ss is sequence of X by RELSET_1:4;
end;
end;
definition
let X be non empty set, s be sequence of X, k be Nat;
redefine func s ^\ k -> subsequence of s;
coherence
proof
set N = (id NAT)^\k;
N is increasing
proof
let e1,e2;
assume e1 in dom N & e2 in dom N;
then reconsider i=e1, j=e2 as Element of NAT;
reconsider jk = j+k, ik = i+k as Element of NAT by ORDINAL1:def 12;
A1: N.j = (id NAT).(jk) by NAT_1:def 3
.= jk;
assume
A2: e1 < e2;
N.i = (id NAT).(ik) by NAT_1:def 3
.= ik;
hence thesis by A1,A2,XREAL_1:6;
end;
then reconsider N as increasing sequence of NAT;
thus s ^\ k is subsequence of s
proof take N;
thus s^\k = (s* id NAT)^\k by FUNCT_2:17
.= s * N by NAT_1:50;
end;
end;
end;
reserve s,s1,s2,s3 for sequence of X;
reserve XX for non empty set,
ss,ss1,ss2,ss3 for sequence of XX;
theorem
ss is subsequence of ss
proof
take id NAT;
thus thesis by FUNCT_2:17;
end;
theorem
ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies
ss1 is subsequence of ss3
proof
given N1 being increasing sequence of NAT such that
A1: ss1 = ss2*N1;
given N2 being increasing sequence of NAT such that
A2: ss2 = ss3*N2;
take N2*N1;
thus thesis by A1,A2,RELAT_1:36;
end;
:: to be generalized to Function of X,Y
registration
let X;
cluster constant for sequence of X;
existence
proof
per cases;
suppose X = {};
then reconsider s = {} as sequence of X by FUNCT_2:def 1,RELSET_1:12;
take s;
thus thesis;
end;
suppose X <> {};
then consider x being object 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;
thus thesis;
end;
end;
end;
theorem Th21:
for ss1 being subsequence of ss holds rng ss1 c= rng ss
proof
let ss1 be subsequence of ss;
let x be object;
consider N being increasing sequence of NAT such that
A1: ss1 = ss * N by Def13;
assume x in rng ss1;
then consider n being object 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 thesis by A4,FUNCT_2:4;
end;
registration
let X be non empty set;
let s be constant sequence of X;
cluster -> constant for subsequence of s;
coherence
proof
let s1 be subsequence of s;
rng s1 c= rng s by Th21;
hence thesis;
end;
end;
:: from FRECHET2, 2008.09.08, A.T.
definition
let X be non empty set, N be increasing sequence of NAT, s be sequence of X;
redefine func s*N -> subsequence of s;
correctness by Def13;
end;
:: from RFUNCT_2 etc. 2008.09.10, A.T.
reserve X,Y for non empty set,
Z for set;
reserve s,s1 for sequence of X,
h,h1 for PartFunc of X,Y,
h2 for PartFunc of Y ,Z,
x for Element of X,
N for increasing sequence of NAT;
theorem
rng s c= dom h & s1 is subsequence of s implies h/*s1 is subsequence of h/*s
proof
assume that
A1: rng s c= dom h and
A2: s1 is subsequence of s;
consider N such that
A3: s1=s*N by A2,Def13;
take N;
thus thesis by A1,A3,FUNCT_2:110;
end;
:: to be generalized
registration
let X be with_non-empty_element set;
cluster non-empty for sequence of X;
existence
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;
thus thesis;
end;
end;
registration
let X be with_non-empty_element set, s be non-empty sequence of X;
cluster -> non-empty for subsequence of s;
coherence
proof
let s1 be subsequence of s;
rng s1 c= rng s by Th21;
hence not {} in rng s1;
end;
end;
reserve i,j for Nat;
definition
let X be non empty set, s be sequence of X;
redefine attr s is constant means
ex x being Element of X st for n being Nat holds s.n=x;
compatibility
proof
hereby
assume s is constant;
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;
take x;
let n be Nat;
dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
hence s.n = x by A1;
end;
given x be Element of X such that
A2: for n being Nat holds s.n=x;
take x;
thus thesis by A2;
end;
end;
theorem Th23:
for X being set for s being constant sequence of X holds s.i = s.j
proof
let X be set;
let s be constant sequence of X;
per cases;
suppose
A1: X is empty;
then s.i = {};
hence thesis by A1;
end;
suppose X is not empty;
then dom s = NAT by FUNCT_2:def 1;
then i in dom s & j in dom s by ORDINAL1:def 12;
hence thesis by FUNCT_1:def 10;
end;
end;
theorem
(for i,j holds s.i = s.j) implies s is constant;
theorem
(for i holds s.i = s.(i+1)) implies s is constant
proof
assume
A1: for i holds s.i = s.(i+1);
now
let i,j;
A2: now
let i,j such that
A3: i <= j;
defpred P[Nat] means i <= $1 implies s.i = s.$1;
A4: for j being Nat st P[j] holds P[j+1]
proof
let j being Nat such that
A5: P[j];
assume i <= j+1;
then i < j+1 or i = j+1 by XXREAL_0:1;
hence thesis by A1,A5,NAT_1:13;
end;
A6: P[0] by NAT_1:3;
for j being Nat holds P[j] from NAT_1:sch 2(A6,A4);
hence s.i = s.j by A3;
end;
i <= j or j <= i;
hence s.i = s.j by A2;
end;
hence thesis;
end;
theorem
s is constant & s1 is subsequence of s implies s = s1
proof
assume that
A1: s is constant and
A2: s1 is subsequence of s;
let n be Element of NAT;
consider N such that
A3: s1=s*N by A2,Def13;
thus s1.n=s.(N.n) by A3,FUNCT_2:15
.=s.n by A1,Th23;
end;
reserve n for Nat;
theorem Th27:
rng s c= dom h implies (h/*s)^\n=h/*(s^\n)
proof
assume
A1: rng s c= dom h;
let m be Element of NAT;
A2: rng (s^\n) c= rng s by Th21;
reconsider mn = m+n as Element of NAT by ORDINAL1:def 12;
thus ((h/*s)^\n).m = (h/*s).(m+n) by NAT_1:def 3
.= h.(s.(mn)) 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;
end;
theorem Th28:
s.n in rng s
proof
n in NAT by ORDINAL1:def 12;
hence thesis by FUNCT_2:112;
end;
theorem
h is total implies h/*(s^\n) = (h/*s)^\n
proof
assume h is total;
then dom h = X by PARTFUN1:def 2;
then rng s c= dom h;
hence thesis by Th27;
end;
theorem Th30:
rng s c= dom h implies h.:(rng s) = rng (h/*s)
proof
assume
A1: rng s c= dom h;
now
let r be Element of Y;
thus r in h.:(rng s) implies r in rng (h/*s)
proof
assume r in h.:(rng 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 thesis by Th28;
end;
assume r in rng (h/*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;
end;
hence thesis by SUBSET_1:3;
end;
theorem
rng s c= dom (h2*h1) implies h2/*(h1/*s) = (h2*h1)/*s
proof
assume
A1: rng s c= dom (h2*h1);
now
let n be Element of NAT;
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;
end;
hence thesis;
end;
definition
let f be ext-real-valued Function;
attr f is zeroed means
f.{} = 0;
end;
:: new, 2009.02.03, A.T.
registration
cluster COMPLEX-valued -> complex-valued for Relation;
coherence;
cluster ExtREAL-valued -> ext-real-valued for Relation;
coherence;
cluster REAL-valued -> real-valued for Relation;
coherence;
cluster NAT-valued -> natural-valued for Relation;
coherence;
end;
definition
let s be ManySortedSet of NAT;
redefine attr s is constant means
ex x being set st for n being Nat holds s.n=x;
compatibility
proof
A1: dom s = NAT by PARTFUN1:def 2;
hereby
assume
A2: s is constant;
take x = s.0;
let n be Nat;
0 in dom s & n in dom s by A1,ORDINAL1:def 12;
hence s.n = x by A2;
end;
given x being set such that
A3: for n being Nat holds s.n=x;
let n1,n2 be object;
assume
A4: n1 in dom s & n2 in dom s;
hence s.n1 = x by A3 .= s.n2 by A3,A4;
end;
end;
theorem
for x being non empty set, M be ManySortedSet of NAT,
s be subsequence of M
holds rng s c= rng M by Lm1;
registration
let X be set;
cluster natural-valued for ManySortedSet of X;
existence
proof
take X --> 0;
thus thesis;
end;
end;