VALUED_0

:: Number-Valued Functions
::  by Library Committee
::
:: Received November 22, 2007
:: Copyright (c) 2007-2026 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;
 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;
  attr f is rational-valued means
  :Def3r:
  rng f c= RAT;
  attr f is integer-valued means
  :Def3i:
  rng f c= INT;
  attr f is natural-valued means
  :Def4:
  rng f c= NAT;
end;

registration
  cluster natural-valued -> integer-valued for Relation;
  coherence
  proof
    let R be Relation;
    assume rng R c= NAT;
    hence rng R c= INT by NUMBERS:17;
  end;
  cluster integer-valued -> rational-valued for Relation;
  coherence
  proof
    let R be Relation;
    assume rng R c= INT;
    hence rng R c= RAT by NUMBERS:14;
  end;
  cluster integer-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 rational-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 -> rational-valued for Relation;
  coherence;
  cluster natural-valued -> real-valued for Relation;
  coherence;
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 rational-valued Relation;
  cluster rng R -> rational-membered;
  coherence
  proof
    rng R c= RAT by Def3r;
    hence thesis;
  end;
end;

registration
  let R be integer-valued Relation;
  cluster rng R -> integer-membered;
  coherence
  proof
    rng R c= INT by Def3i;
    hence thesis;
  end;
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 Th4:
  for S being rational-valued Relation st R c= S holds R is rational-valued
proof
  let S be rational-valued Relation;
  assume R c= S;
  then
A1: rng R c= rng S by RELAT_1:11;
  rng S c= RAT by Def3r;
  hence rng R c= RAT by A1;
end;

theorem Th5:
  for S being integer-valued Relation st R c= S holds R is integer-valued
proof
  let S be integer-valued Relation;
  assume R c= S;
  then
A1: rng R c= rng S by RELAT_1:11;
  rng S c= INT by Def3i;
  hence rng R c= INT by A1;
end;

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 rational-valued Relation;
  cluster -> rational-valued for Subset of R;
  coherence by Th4;
end;

registration
  let R be integer-valued Relation;
  cluster -> integer-valued for Subset of R;
  coherence by Th5;
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 rational-valued Relation;
  cluster R \/ S -> rational-valued;
  coherence
  proof
A1: rng(R \/ S) = rng R \/ rng S by RELAT_1:12;
    rng R c= RAT & rng S c= RAT by Def3r;
    hence rng(R \/ S) c= RAT by A1,XBOOLE_1:8;
  end;
end;

registration
  let R,S be integer-valued Relation;
  cluster R \/ S -> integer-valued;
  coherence
  proof
A1: rng(R \/ S) = rng R \/ rng S by RELAT_1:12;
    rng R c= INT & rng S c= INT by Def3i;
    hence rng(R \/ S) c= INT by A1,XBOOLE_1:8;
  end;
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 rational-valued Relation;
  let S;
  cluster R /\ S -> rational-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= RAT by Def3r;
    hence rng(R /\ S) c= RAT by A1;
  end;
  cluster R \ S -> rational-valued;
  coherence;
end;

registration
  let R be integer-valued Relation;
  let S;
  cluster R /\ S -> integer-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= INT by Def3i;
    hence rng(R /\ S) c= INT by A1;
  end;
  cluster R \ S -> integer-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 rational-valued Relation;
  cluster R \+\ S -> rational-valued;
  coherence;
end;

registration
  let R,S be integer-valued Relation;
  cluster R \+\ S -> integer-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 rational-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 integer-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 rational-valued Relation;
  let x;
  cluster Im(R,x) -> rational-membered;
  coherence;
end;

registration
  let R be integer-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 rational-valued Relation;
  let X;
  cluster R|X -> rational-valued;
  coherence
  proof
    rng R c= RAT & rng(R|X) c= rng R by Def3r,RELAT_1:70;
    hence rng(R|X) c= RAT;
  end;
end;

registration
  let R be integer-valued Relation;
  let X;
  cluster R|X -> integer-valued;
  coherence
  proof
    rng R c= INT & rng(R|X) c= rng R by Def3i,RELAT_1:70;
    hence rng(R|X) c= INT;
  end;
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 -> rational-valued;
  coherence
  by MEMBERED:4;
end;

registration
  let X be integer-membered set;
  cluster id X -> integer-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 rational-valued Relation;
  cluster R*S -> rational-valued;
  coherence
  proof
    rng S c= RAT & rng(R*S) c= rng S by Def3r,RELAT_1:26;
    hence rng(R*S) c= RAT;
  end;
end;

registration
  let R;
  let S be integer-valued Relation;
  cluster R*S -> integer-valued;
  coherence
  proof
    rng S c= INT & rng(R*S) c= rng S by Def3i,RELAT_1:26;
    hence rng(R*S) c= INT;
  end;
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  :: redefines complex-valued (VALUED_0, definition)
  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  :: redefines ext-real-valued (VALUED_0, definition)

  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  :: redefines real-valued (VALUED_0, definition)
  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;
  redefine attr f is rational-valued means  :: redefines rational-valued (VALUED_0, definition)
  for x st x in dom f holds f.x is rational;
  compatibility
  proof
    thus f is rational-valued implies for x st x in dom f holds f.x is rational
    proof
      assume
A7:   f is rational-valued;
      let x;
      assume
A8:   x in dom f;
      reconsider f as rational-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 rational;
    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 rational by A9;
    hence thesis by RAT_1:def 2;
  end;
  redefine attr f is integer-valued means  :: redefines integer-valued (VALUED_0, definition)
  for x st x in dom f holds f.x is integer;
  compatibility
  proof
    thus f is integer-valued implies for x st x in dom f holds f.x is integer
    proof
      assume
A7:   f is integer-valued;
      let x;
      assume
A8:   x in dom f;
      reconsider f as integer-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 integer;
    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 integer by A9;
    hence thesis by INT_1:def 2;
  end;
  redefine attr f is natural-valued means  :: redefines natural-valued (VALUED_0, definition)
  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;
  thus 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;
  thus 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;
  thus thesis;
end;

theorem Th10:
  f is rational-valued iff for x holds f.x is rational
proof
  hereby
    assume
A1: f is rational-valued;
    let x;
    per cases;
    suppose
      x in dom f;
      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;
  thus thesis;
end;

theorem Th11:
  f is integer-valued iff for x holds f.x is integer
proof
  hereby
    assume
A1: f is integer-valued;
    let x;
    per cases;
    suppose
      x in dom f;
      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;
  thus thesis;
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;
  thus 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 rational-valued Function;
  let x be object;
  cluster f.x -> rational;
  coherence by Th10;
end;

registration
  let f be integer-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 -> rational-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 -> integer-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;
    hence thesis by MEMBERED:1;
  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;
    hence thesis by MEMBERED:2;
  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;
    hence thesis by MEMBERED:3;
  end;
end;

registration
  let f,g be rational-valued Function;
  cluster f +* g -> rational-valued;
  coherence
  proof
    rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
    hence thesis by MEMBERED:4;
  end;
end;

registration
  let f,g be integer-valued Function;
  cluster f +* g -> integer-valued;
  coherence
  proof
    rng(f +* g) c= rng f \/ rng g by FUNCT_4:17;
    hence thesis by MEMBERED:5;
  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;
    hence thesis by MEMBERED:6;
  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 -> rational-valued;
  coherence;
end;

registration
  let x;
  let y be Integer;
  cluster x .--> y -> integer-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 -> rational-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 -> integer-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:] -> rational-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:] -> integer-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 integer-valued rational-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 rational-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 rational-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 integer-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 integer-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;  :: redefines subsequence (VALUED_0, definition)
  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;  :: redefines ^\ (NAT_1, definition)
  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;  :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
  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  :: redefines constant (FUNCT_1, definition)
  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 complex-valued -> COMPLEX-valued for Relation;
  coherence;
  cluster ExtREAL-valued -> ext-real-valued for Relation;
  coherence;
  cluster ext-real-valued -> ExtREAL-valued for Relation;
  coherence;
  cluster REAL-valued -> real-valued for Relation;
  coherence;
  cluster real-valued -> REAL-valued for Relation;
  coherence;
  cluster RAT-valued -> rational-valued for Relation;
  coherence;
  cluster rational-valued -> RAT-valued for Relation;
  coherence;
  cluster INT-valued -> integer-valued for Relation;
  coherence;
  cluster integer-valued -> INT-valued for Relation;
  coherence;
  cluster NAT-valued -> natural-valued for Relation;
  coherence;
  cluster natural-valued -> NAT-valued for Relation;
  coherence;
end;

definition
  let s be ManySortedSet of NAT;
  redefine attr s is constant means  :: redefines constant (FUNCT_1, definition)
  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;

:: Added by AK, 13.12.2022

registration
  let D be complex-membered set;
  cluster D-valued -> COMPLEX-valued for Relation;
  coherence by MEMBERED:1;
end;

registration
  let D be complex-membered set;
  cluster D-valued -> complex-valued for Relation;
  coherence;
end;

registration
  let D be ext-real-membered set;
  cluster D-valued -> ExtREAL-valued for Relation;
  coherence by MEMBERED:2;
end;

registration
  let D be ext-real-membered set;
  cluster D-valued -> ext-real-valued for Relation;
  coherence;
end;

registration
  let D be real-membered set;
  cluster D-valued -> REAL-valued for Relation;
  coherence by MEMBERED:3;
end;

registration
  let D be real-membered set;
  cluster D-valued -> real-valued for Relation;
  coherence;
end;

registration
  let D be rational-membered set;
  cluster D-valued -> RAT-valued for Relation;
  coherence by MEMBERED:4;
end;

registration
  let D be rational-membered set;
  cluster D-valued -> rational-valued for Relation;
  coherence;
end;

registration
  let D be integer-membered set;
  cluster D-valued -> INT-valued for Relation;
  coherence by MEMBERED:5;
end;

registration
  let D be integer-membered set;
  cluster D-valued -> integer-valued for Relation;
  coherence;
end;

registration
  let D be natural-membered set;
  cluster D-valued -> NAT-valued for Relation;
  coherence by MEMBERED:6;
end;

registration
  let D be natural-membered set;
  cluster D-valued -> natural-valued for Relation;
  coherence;
end;

registration
  let f be increasing ext-real-valued Function;
  let X be set;
  cluster f|X -> increasing;
  coherence
  proof
    set g = f|X;
    let e1,e2 be ExtReal such that
A1: e1 in dom g & e2 in dom g;
A2: dom g c= dom f by RELAT_1:60;
    f.e1 = g.e1 & f.e2 = g.e2 by A1,FUNCT_1:47;
    hence thesis by A1,A2,Def9;
  end;
end;

registration
  let f be non-increasing ext-real-valued Function;
  let X be set;
  cluster f|X -> non-increasing;
  coherence
  proof
    set g = f|X;
    let e1,e2 be ExtReal such that
A1: e1 in dom g & e2 in dom g;
A2: dom g c= dom f by RELAT_1:60;
    f.e1 = g.e1 & f.e2 = g.e2 by A1,FUNCT_1:47;
    hence thesis by A1,A2,Def12;
  end;
end;

registration
  let f be decreasing ext-real-valued Function;
  let X be set;
  cluster f|X -> decreasing;
  coherence
  proof
    set g = f|X;
    let e1,e2 be ExtReal such that
A1: e1 in dom g & e2 in dom g;
A2: dom g c= dom f by RELAT_1:60;
    f.e1 = g.e1 & f.e2 = g.e2 by A1,FUNCT_1:47;
    hence thesis by A1,A2,Def10;
  end;
end;

registration
  let f be non-decreasing ext-real-valued Function;
  let X be set;
  cluster f|X -> non-decreasing;
  coherence
  proof
    set g = f|X;
    let e1,e2 be ExtReal such that
A1: e1 in dom g & e2 in dom g;
A2: dom g c= dom f by RELAT_1:60;
    f.e1 = g.e1 & f.e2 = g.e2 by A1,FUNCT_1:47;
    hence thesis by A1,A2,Def11;
  end;
end;