:: Properties of Number-Valued Functions
::  by Library Committee
::
:: Received December 18, 2007
:: Copyright (c) 2007-2018 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, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, ORDINAL1,
      XXREAL_0, VALUED_0, RAT_1, COMPLEX1, ARYTM_1, ARYTM_3, MEMBERED,
      PARTFUN1, TARSKI, SUBSET_1, CARD_1, XCMPLX_0, INT_1, SQUARE_1, FUNCT_4,
      FINSET_1, NAT_1, ORDINAL2, VALUED_1, AMISTD_1, FUNCOP_1, AMISTD_2,
      AMISTD_3, ORDINAL4, REAL_1, XREAL_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, XCMPLX_0,
      NUMBERS, COMPLEX1, XXREAL_0, XXREAL_2, FUNCOP_1, XREAL_0, RAT_1, INT_1,
      INT_2, SQUARE_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4,
      FINSEQ_1, MEMBERED, NAT_1, VALUED_0;
 constructors PARTFUN1, RAT_1, VALUED_0, SQUARE_1, MEMBERED, INT_2, FINSEQ_1,
      NAT_1, FUNCT_4, NAT_D, RELSET_1, XXREAL_2, FUNCOP_1, DOMAIN_1, WELLORD2,
      FINSEQ_3, REAL_1;
 registrations ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
      VALUED_0, RAT_1, INT_1, NAT_1, FUNCT_1, FINSET_1, XXREAL_0, RELAT_1,
      XXREAL_2, FUNCOP_1, FUNCT_4, CARD_1, FINSEQ_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0,
      WELLORD2;
 equalities XBOOLE_0, XCMPLX_0, SQUARE_1, FINSEQ_1, FUNCOP_1;
 expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, VALUED_0, WELLORD2;
 theorems FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, VALUED_0, COMPLEX1, FINSEQ_1,
      XBOOLE_0, TARSKI, GRFUNC_1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, INT_1,
      ORDINAL1, XXREAL_0, FUNCOP_1, ZFMISC_1, XXREAL_2, XBOOLE_1, CARD_1,
      CARD_2, RAT_1, XTUPLE_0, XREAL_1, FINSEQ_3;
 schemes FUNCT_1, CLASSES1, FRAENKEL, RECDEF_1, NAT_1;

begin :: f1 + f2

Lm1: for f being FinSequence, h being Function st dom h = dom f holds h is
FinSequence
proof
  let f be FinSequence, h be Function such that
A1: dom h = dom f;
  h is FinSequence-like
  proof
    take len f;
    thus thesis by A1,FINSEQ_1:def 3;
  end;
  hence thesis;
end;

Lm2: for f, g being FinSequence, h being Function st dom h = dom f /\ dom g
holds h is FinSequence
proof
  let f, g be FinSequence, h be Function such that
A1: dom h = dom f /\ dom g;
  consider n being Nat such that
A2: dom f = Seg n by FINSEQ_1:def 2;
  consider m being Nat such that
A3: dom g = Seg m by FINSEQ_1:def 2;
  h is FinSequence-like
  proof
    per cases;
    suppose
A4:   n <= m;
      take n;
      thus thesis by A1,A2,A3,A4,FINSEQ_1:7;
    end;
    suppose
A5:   m <= n;
      take m;
      thus thesis by A1,A2,A3,A5,FINSEQ_1:7;
    end;
  end;
  hence thesis;
end;

registration
  cluster complex-valued for FinSequence;
  existence
  proof
    take <*>COMPLEX;
    thus thesis;
  end;
end;
:: move somewhere

registration
  let r be Rational;
  cluster |. r .| -> rational;
  coherence
  proof
    |. r .| = -r or |. r .| = r by COMPLEX1:71;
    hence thesis;
  end;
end;

definition
  let f1,f2 be complex-valued Function;
  deffunc F(object) = f1.$1 + f2.$1;
  set X = dom f1 /\ dom f2;
  func f1 + f2 -> Function means
  :Def1:
  dom it = dom f1 /\ dom f2 &
  for c being object st c in dom it holds it.c = f1.c + f2.c;
  existence
  proof
    ex f being Function st dom f = X & for x being object st x in X holds f.x
    = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let f, g be Function such that
A1: dom f = X and
A2: for c being object st c in dom f holds f.c = F(c) and
A3: dom g = X and
A4: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A5:   x in dom f;
      hence f.x = F(x) by A2
        .= g.x by A1,A3,A4,A5;
    end;
    hence thesis by A1,A3;
  end;
  commutativity;
end;

registration
  let f1,f2 be complex-valued Function;
  cluster f1+f2 -> complex-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1+f2);
    then (f1+f2).x = f1.x + f2.x by Def1;
    hence thesis;
  end;
end;

registration
  let f1,f2 be real-valued Function;
  cluster f1+f2 -> real-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1+f2);
    then (f1+f2).x = f1.x + f2.x by Def1;
    hence thesis;
  end;
end;

registration
  let f1,f2 be RAT-valued Function;
  cluster f1+f2 -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng(f1+f2);
    then consider x being object such that
A1: x in dom (f1+f2) and
A2: (f1+f2).x = y by FUNCT_1:def 3;
    (f1+f2).x = f1.x + f2.x by A1,Def1;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

registration
  let f1,f2 be INT-valued Function;
  cluster f1+f2 -> INT-valued;
  coherence
  proof
    let y be object;
    assume y in rng(f1+f2);
    then consider x being object such that
A1: x in dom (f1+f2) and
A2: (f1+f2).x = y by FUNCT_1:def 3;
    (f1+f2).x = f1.x + f2.x by A1,Def1;
    hence thesis by A2,INT_1:def 2;
  end;
end;

registration
  let f1,f2 be natural-valued Function;
  cluster f1+f2 -> natural-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1+f2);
    then (f1+f2).x = f1.x + f2.x by Def1;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D1,D2 be complex-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1+f2 -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= COMPLEX by Def1,
VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be real-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1+f2 -> PartFunc of C,REAL;
  coherence
  proof
    dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= REAL by Def1,VALUED_0:def 3
;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be rational-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1+f2 -> PartFunc of C,RAT;
  coherence
  proof
    dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= RAT by Def1,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be integer-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1+f2 -> PartFunc of C,INT;
  coherence
  proof
    dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= INT by Def1,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be natural-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1+f2 -> PartFunc of C,NAT;
  coherence
  proof
    dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= NAT by Def1,VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1+f2 -> total for PartFunc of C,COMPLEX;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1+f2) = C /\ C by Def1
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be real-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1+f2 -> total for PartFunc of C,REAL;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1+f2) = C /\ C by Def1
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be rational-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1+f2 -> total for PartFunc of C,RAT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1+f2) = C /\ C by Def1
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be integer-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1+f2 -> total for PartFunc of C,INT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1+f2) = C /\ C by Def1
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be natural-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1+f2 -> total for PartFunc of C,NAT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1+f2) = C /\ C by Def1
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

theorem
  for C being set, D1,D2 being complex-membered non empty set for f1
  being Function of C,D1, f2 being Function of C,D2 for c being Element of C
  holds (f1+f2).c = f1.c + f2.c
proof
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1, f2 be Function of C,D2;
A1: dom(f1+f2) = C by FUNCT_2:def 1;
  let c be Element of C;
  per cases;
  suppose
    C is non empty;
    hence thesis by A1,Def1;
  end;
  suppose
A2: C is empty;
    then f1.c = 0;
    hence thesis by A2;
  end;
end;

registration
  let f1, f2 be complex-valued FinSequence;
  cluster f1+f2 -> FinSequence-like;
  coherence
  proof
    dom(f1+f2) = dom f1 /\ dom f2 by Def1;
    hence thesis by Lm2;
  end;
end;

begin :: r + f

definition
  let f be complex-valued Function, r be Complex;
  deffunc F(object) = r + f.$1;
  func r + f -> Function means
  :Def2:
  dom it = dom f &
  for c being object st c in dom it holds it.c = r + f.c;
  existence
  proof
    ex g being Function st dom g = dom f & for x being object st x in dom f
    holds g.x = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let h, g be Function such that
A1: dom h = dom f and
A2: for c being object st c in dom h holds h.c = F(c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A5:   x in dom h;
      hence h.x = F(x) by A2
        .= g.x by A1,A3,A4,A5;
    end;
    hence thesis by A1,A3;
  end;
end;

notation
  let f be complex-valued Function, r be Complex;
  synonym f + r for r + f;
end;

registration
  let f be complex-valued Function, r be Complex;
  cluster r+f -> complex-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r+f);
    then (r+f).x = r + f.x by Def2;
    hence thesis;
  end;
end;

registration
  let f be real-valued Function, r be Real;
  cluster r+f -> real-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r+f);
    then (r+f).x = r + f.x by Def2;
    hence thesis;
  end;
end;

registration
  let f be RAT-valued Function, r be Rational;
  cluster r+f -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (r+f);
    then consider x being object such that
A1: x in dom (r+f) and
A2: (r+f).x = y by FUNCT_1:def 3;
    (r+f).x = r + f.x by A1,Def2;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

registration
  let f be INT-valued Function, r be Integer;
  cluster r+f -> INT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (r+f);
    then consider x being object such that
A1: x in dom (r+f) and
A2: (r+f).x = y by FUNCT_1:def 3;
    (r+f).x = r + f.x by A1,Def2;
    hence thesis by A2,INT_1:def 2;
  end;
end;

registration
  let f be natural-valued Function, r be Nat;
  cluster r+f -> natural-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r+f);
    then (r+f).x = r + f.x by Def2;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  let r be Complex;
  redefine func r+f -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (r+f) = dom f & rng (r+f) c= COMPLEX by Def2,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  let r be Real;
  redefine func r+f -> PartFunc of C,REAL;
  coherence
  proof
    dom (r+f) = dom f & rng (r+f) c= REAL by Def2,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  let r be Rational;
  redefine func r+f -> PartFunc of C,RAT;
  coherence
  proof
    dom (r+f) = dom f & rng (r+f) c= RAT by Def2,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  let r be Integer;
  redefine func r+f -> PartFunc of C,INT;
  coherence
  proof
    dom (r+f) = dom f & rng (r+f) c= INT by Def2,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be natural-membered set;
  let f be PartFunc of C,D;
  let r be Nat;
  redefine func r+f -> PartFunc of C,NAT;
  coherence
  proof
    dom (r+f) = dom f & rng (r+f) c= NAT by Def2,VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  let r be Complex;
  cluster r+f -> total for PartFunc of C,COMPLEX;
  coherence
  proof
    dom(r+f) = dom f by Def2
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  let r be Real;
  cluster r+f -> total for PartFunc of C,REAL;
  coherence
  proof
    dom(r+f) = dom f by Def2
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  let r be Rational;
  cluster r+f -> total for PartFunc of C,RAT;
  coherence
  proof
    dom(r+f) = dom f by Def2
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  let r be Integer;
  cluster r+f -> total for PartFunc of C,INT;
  coherence
  proof
    dom(r+f) = dom f by Def2
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be natural-membered non empty set;
  let f be Function of C,D;
  let r be Nat;
  cluster r+f -> total for PartFunc of C,NAT;
  coherence
  proof
    dom(r+f) = dom f by Def2
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

theorem
  for C being non empty set, D being complex-membered non empty set
  for f being Function of C,D, r being Complex
  for c being Element of C holds
  (r+f).c = r + f.c
proof
  let C be non empty set;
  let D be complex-membered non empty set;
  let f be Function of C,D, r be Complex;
  dom(r+f) = C by FUNCT_2:def 1;
  hence thesis by Def2;
end;

registration
  let f be complex-valued FinSequence, r be Complex;
  cluster r+f -> FinSequence-like;
  coherence
  proof
    dom (r+f) = dom f by Def2;
    hence thesis by Lm1;
  end;
end;

begin :: f - r

definition
  let f be complex-valued Function, r be Complex;
  func f - r -> Function equals
  -r + f;
  coherence;
end;

theorem
  for f being complex-valued Function, r being Complex holds dom
  (f-r) = dom f & for c being object st c in dom f holds (f-r).c = f.c - r
proof
  let f be complex-valued Function, r be Complex;
  dom (f-r) = dom f by Def2;
  hence thesis by Def2;
end;

registration
  let f be complex-valued Function, r be Complex;
  cluster f-r -> complex-valued;
  coherence;
end;

registration
  let f be real-valued Function, r be Real;
  cluster f-r -> real-valued;
  coherence;
end;

registration
  let f be RAT-valued Function, r be Rational;
  cluster f-r -> RAT-valued;
  coherence;
end;

registration
  let f be INT-valued Function, r be Integer;
  cluster f-r -> INT-valued;
  coherence;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  let r be Complex;
  redefine func f-r -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f-r) = dom f & rng (f-r) c= COMPLEX by Def2,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  let r be Real;
  redefine func f-r -> PartFunc of C,REAL;
  coherence
  proof
    dom (f-r) = dom f & rng (f-r) c= REAL by Def2,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  let r be Rational;
  redefine func f-r -> PartFunc of C,RAT;
  coherence
  proof
    dom (f-r) = dom f & rng (f-r) c= RAT by Def2,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  let r be Integer;
  redefine func f-r -> PartFunc of C,INT;
  coherence
  proof
    dom (f-r) = dom f & rng (f-r) c= INT by Def2,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  let r be Complex;
  cluster f-r -> total for PartFunc of C,COMPLEX;
  coherence;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  let r be Real;
  cluster f-r -> total for PartFunc of C,REAL;
  coherence;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  let r be Rational;
  cluster f-r -> total for PartFunc of C,RAT;
  coherence;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  let r be Integer;
  cluster f-r -> total for PartFunc of C,INT;
  coherence;
end;

theorem
  for C being non empty set, D being complex-membered non empty set for
f being Function of C,D, r being Complex for c being Element of C holds
  (f-r).c = f.c - r
proof
  let C be non empty set;
  let D be complex-membered non empty set;
  let f be Function of C,D, r be Complex;
  dom (f-r) = C by FUNCT_2:def 1;
  hence thesis by Def2;
end;

registration
  let f be complex-valued FinSequence, r be Complex;
  cluster f-r -> FinSequence-like;
  coherence;
end;

begin :: f1 (#) f2

definition
  let f1,f2 be complex-valued Function;
  deffunc F(object) = f1.$1 * f2.$1;
  set X = dom f1 /\ dom f2;
  func f1 (#) f2 -> Function means
  :Def4:
  dom it = dom f1 /\ dom f2 & for c
  being object st c in dom it holds it.c = f1.c * f2.c;
  existence
  proof
    ex f being Function st dom f = X & for x being object st x in X holds f.x
    = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let f, g be Function such that
A1: dom f = X and
A2: for c being object st c in dom f holds f.c = F(c) and
A3: dom g = X and
A4: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A5:   x in dom f;
      hence f.x = F(x) by A2
        .= g.x by A1,A3,A4,A5;
    end;
    hence thesis by A1,A3;
  end;
  commutativity;
end;

theorem
  for f1,f2 being complex-valued Function
   for c being object holds (f1(#)f2).c = f1.c * f2.c
proof
  let f1,f2 be complex-valued Function;
  let c be object;
A1: dom (f1(#)f2) = dom f1 /\ dom f2 by Def4;
  per cases;
  suppose
    c in dom (f1(#)f2);
    hence thesis by Def4;
  end;
  suppose
A2: not c in dom (f1(#)f2);
    then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4;
    then f1.c = 0 or f2.c = 0 by FUNCT_1:def 2;
    hence thesis by A2,FUNCT_1:def 2;
  end;
end;

registration
  let f1,f2 be complex-valued Function;
  cluster f1(#)f2 -> complex-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1(#)f2);
    then (f1(#)f2).x = f1.x * f2.x by Def4;
    hence thesis;
  end;
end;

registration
  let f1,f2 be real-valued Function;
  cluster f1(#)f2 -> real-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1(#)f2);
    then (f1(#)f2).x = f1.x * f2.x by Def4;
    hence thesis;
  end;
end;

registration
  let f1,f2 be RAT-valued Function;
  cluster f1(#)f2 -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (f1(#)f2);
    then consider x being object such that
A1: x in dom (f1(#)f2) and
A2: (f1(#)f2).x = y by FUNCT_1:def 3;
    (f1(#)f2).x = f1.x * f2.x by A1,Def4;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

registration
  let f1,f2 be INT-valued Function;
  cluster f1(#)f2 -> INT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (f1(#)f2);
    then consider x being object such that
A1: x in dom (f1(#)f2) and
A2: (f1(#)f2).x = y by FUNCT_1:def 3;
    (f1(#)f2).x = f1.x * f2.x by A1,Def4;
    hence thesis by A2,INT_1:def 2;
  end;
end;

registration
  let f1,f2 be natural-valued Function;
  cluster f1(#)f2 -> natural-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f1(#)f2);
    then (f1(#)f2).x = f1.x * f2.x by Def4;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D1,D2 be complex-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1(#)f2 -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= COMPLEX by Def4,
VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be real-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1(#)f2 -> PartFunc of C,REAL;
  coherence
  proof
    dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= REAL by Def4,
VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be rational-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1(#)f2 -> PartFunc of C,RAT;
  coherence
  proof
    dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= RAT by Def4,
RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be integer-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1(#)f2 -> PartFunc of C,INT;
  coherence
  proof
    dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= INT by Def4,
RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be natural-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1(#)f2 -> PartFunc of C,NAT;
  coherence
  proof
    dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= NAT by Def4,
VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1(#)f2 -> total for PartFunc of C,COMPLEX;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1(#)f2) = C /\ C by Def4
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be real-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1(#)f2 -> total for PartFunc of C,REAL;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1(#)f2) = C /\ C by Def4
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be rational-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1(#)f2 -> total for PartFunc of C,RAT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1(#)f2) = C /\ C by Def4
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be integer-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1(#)f2 -> total for PartFunc of C,INT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1(#)f2) = C /\ C by Def4
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D1,D2 be natural-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1(#)f2 -> total for PartFunc of C,NAT;
  coherence
  proof
    dom f1 = C & dom f2 = C by FUNCT_2:def 1;
    then dom(f1(#)f2) = C /\ C by Def4
      .= C;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let f1, f2 be complex-valued FinSequence;
  cluster f1(#)f2 -> FinSequence-like;
  coherence
  proof
    dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
    hence thesis by Lm2;
  end;
end;

begin :: r (#) f

definition
  let f be complex-valued Function, r be Complex;
  deffunc F(object) = r * f.$1;
  func r (#) f -> Function means
  :Def5:
  dom it = dom f & for c being object st c
  in dom it holds it.c = r * f.c;
  existence
  proof
    ex g being Function st dom g = dom f & for x being object st x in dom f
    holds g.x = F(x) from FUNCT_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    let h, g be Function such that
A1: dom h = dom f and
A2: for c being object st c in dom h holds h.c = F(c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A5:   x in dom h;
      hence h.x = F(x) by A2
        .= g.x by A1,A3,A4,A5;
    end;
    hence thesis by A1,A3;
  end;
end;

notation
  let f be complex-valued Function, r be Complex;
  synonym f (#) r for r (#) f;
end;

theorem Th6:
  for f being complex-valued Function, r being Complex for c
  being object holds (r(#)f).c = r * f.c
proof
  let f be complex-valued Function, r be Complex;
  let c be object;
A1: dom f = dom (r(#)f) by Def5;
  per cases;
  suppose
    c in dom f;
    hence thesis by A1,Def5;
  end;
  suppose
A2: not c in dom f;
    hence (r(#)f).c = r*0 by A1,FUNCT_1:def 2
      .= r * f.c by A2,FUNCT_1:def 2;
  end;
end;

registration
  let f be complex-valued Function, r be Complex;
  cluster r(#)f -> complex-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r(#)f);
    then (r(#)f).x = r * f.x by Def5;
    hence thesis;
  end;
end;

registration
  let f be real-valued Function, r be Real;
  cluster r(#)f -> real-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r(#)f);
    then (r(#)f).x = r * f.x by Def5;
    hence thesis;
  end;
end;

registration
  let f be RAT-valued Function, r be Rational;
  cluster r(#)f -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (r(#)f);
    then consider x being object such that
A1: x in dom (r(#)f) and
A2: (r(#)f).x = y by FUNCT_1:def 3;
    (r(#)f).x = r * f.x by A1,Def5;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

registration
  let f be INT-valued Function, r be Integer;
  cluster r(#)f -> INT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (r(#)f);
    then consider x being object such that
A1: x in dom (r(#)f) and
A2: (r(#)f).x = y by FUNCT_1:def 3;
    (r(#)f).x = r * f.x by A1,Def5;
    hence thesis by A2,INT_1:def 2;
  end;
end;

registration
  let f be natural-valued Function, r be Nat;
  cluster r(#)f -> natural-valued;
  coherence
  proof
    let x be object;
    assume x in dom (r(#)f);
    then (r(#)f).x = r * f.x by Def5;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  let r be Complex;
  redefine func r(#)f -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (r(#)f) = dom f & rng (r(#)f) c= COMPLEX by Def5,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  let r be Real;
  redefine func r(#)f -> PartFunc of C,REAL;
  coherence
  proof
    dom (r(#)f) = dom f & rng (r(#)f) c= REAL by Def5,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  let r be Rational;
  redefine func r(#)f -> PartFunc of C,RAT;
  coherence
  proof
    dom (r(#)f) = dom f & rng (r(#)f) c= RAT by Def5,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  let r be Integer;
  redefine func r(#)f -> PartFunc of C,INT;
  coherence
  proof
    dom (r(#)f) = dom f & rng (r(#)f) c= INT by Def5,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be natural-membered set;
  let f be PartFunc of C,D;
  let r be Nat;
  redefine func r(#)f -> PartFunc of C,NAT;
  coherence
  proof
    dom (r(#)f) = dom f & rng (r(#)f) c= NAT by Def5,VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  let r be Complex;
  cluster r(#)f -> total for PartFunc of C,COMPLEX;
  coherence
  proof
    dom(r(#)f) = dom f by Def5
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  let r be Real;
  cluster r(#)f -> total for PartFunc of C,REAL;
  coherence
  proof
    dom(r(#)f) = dom f by Def5
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  let r be Rational;
  cluster r(#)f -> total for PartFunc of C,RAT;
  coherence
  proof
    dom(r(#)f) = dom f by Def5
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  let r be Integer;
  cluster r(#)f -> total for PartFunc of C,INT;
  coherence
  proof
    dom(r(#)f) = dom f by Def5
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be natural-membered non empty set;
  let f be Function of C,D;
  let r be Nat;
  cluster r(#)f -> total for PartFunc of C,NAT;
  coherence
  proof
    dom(r(#)f) = dom f by Def5
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

theorem
  for C being non empty set, D being complex-membered non empty set for
  f being Function of C,D, r being Complex for g being Function of C,
  COMPLEX st for c being Element of C holds g.c = r * f.c holds g = r(#)f
proof
  let C be non empty set, D be complex-membered non empty set;
  let f be Function of C,D, r be Complex;
  let g be Function of C,COMPLEX such that
A1: for c being Element of C holds g.c = r * f.c;
  let x be Element of C;
  thus g.x = r*f.x by A1
    .= (r(#)f).x by Th6;
end;

registration
  let f be complex-valued FinSequence, r be Complex;
  cluster r(#)f -> FinSequence-like;
  coherence
  proof
    dom (r(#)f) = dom f by Def5;
    hence thesis by Lm1;
  end;
end;

begin :: -f

definition
  let f be complex-valued Function;
  func -f -> complex-valued Function equals
  (-1) (#) f;
  coherence;
  involutiveness
  proof
    let r, h be complex-valued Function;
    assume
A1: r = (-1)(#)h;
    thus dom ((-1)(#)r) = dom r by Def5
      .= dom h by A1,Def5;
    let c be object;
    assume c in dom h;
    reconsider a = (-1)*(h.c) as Complex;
    thus h.c = (-1) * a
      .= (-1)*r.c by A1,Th6
      .= ((-1)(#)r).c by Th6;
  end;
end;

theorem Th8:
  for f being complex-valued Function holds dom -f = dom f & for c
  being object holds (-f).c = -(f.c)
proof
  let f be complex-valued Function;
  thus
A1: dom -f = dom f by Def5;
  let c be object;
  per cases;
  suppose
    c in dom f;
    hence (-f).c = (-1)*f.c by A1,Def5
      .= -(f.c);
  end;
  suppose
A2: not c in dom f;
    hence (-f).c = -(0 qua Complex) by A1,FUNCT_1:def 2
      .= -(f.c) by A2,FUNCT_1:def 2;
  end;
end;

theorem
  for f being complex-valued Function, g being Function st dom f = dom g
  & for c being object st c in dom f holds g.c = -(f.c) holds g = -f
proof
  let f be complex-valued Function, g be Function;
  assume that
A1: dom f = dom g and
A2: for c being object st c in dom f holds g.c = -(f.c);
  thus dom -f = dom g by A1,Def5;
  let c be object;
  assume
A3: c in dom g;
  thus (-f).c = -f.c by Th8
    .= g.c by A1,A2,A3;
end;

registration
  let f be complex-valued Function;
  cluster -f -> complex-valued;
  coherence;
end;

registration
  let f be real-valued Function;
  cluster -f -> real-valued;
  coherence;
end;

registration
  let f be RAT-valued Function;
  cluster -f -> RAT-valued;
  coherence;
end;

registration
  let f be INT-valued Function;
  cluster -f -> INT-valued;
  coherence;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  redefine func -f -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom -f = dom f & rng -f c= COMPLEX by Def5,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  redefine func -f -> PartFunc of C,REAL;
  coherence
  proof
    dom -f = dom f & rng -f c= REAL by Def5,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  redefine func -f -> PartFunc of C,RAT;
  coherence
  proof
    dom -f = dom f & rng -f c= RAT by Def5,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  redefine func -f -> PartFunc of C,INT;
  coherence
  proof
    dom -f = dom f & rng -f c= INT by Def5,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  cluster -f -> total for PartFunc of C,COMPLEX;
  coherence;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  cluster -f -> total for PartFunc of C,REAL;
  coherence;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  cluster -f -> total for PartFunc of C,RAT;
  coherence;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  cluster -f -> total for PartFunc of C,INT;
  coherence;
end;

registration
  let f be complex-valued FinSequence;
  cluster -f -> FinSequence-like;
  coherence;
end;

begin :: f"

definition
  let f be complex-valued Function;
  deffunc F(object) = (f.$1)";
  func f" -> complex-valued Function means
  :Def7:
  dom it = dom f & for c being
  object st c in dom it holds it.c = (f.c)";
  existence
  proof
    consider g being Function such that
A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x)
    from FUNCT_1:sch 3;
    g is complex-valued
    proof
      let x be object;
      assume x in dom g;
      then g.x = (f.x)" by A1;
      hence thesis;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let h, g be complex-valued Function such that
A2: dom h = dom f and
A3: for c being object st c in dom h holds h.c = F(c) and
A4: dom g = dom f and
A5: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A6:   x in dom h;
      hence h.x = F(x) by A3
        .= g.x by A2,A4,A5,A6;
    end;
    hence thesis by A2,A4;
  end;
  involutiveness
  proof
    let r, h be complex-valued Function;
    assume that
A7: dom r = dom h and
A8: for c being object st c in dom r holds r.c = (h.c)";
    thus dom r = dom h by A7;
    let c be object;
    assume
A9: c in dom h;
    thus h.c = (h.c)""
      .= (r.c)" by A7,A8,A9;
  end;
end;
::better name

theorem Th10:
  for f being complex-valued Function for c being object holds
  f".c = (f.c)"
proof
  let f be complex-valued Function;
  let c be object;
A1: dom (f") = dom f by Def7;
  per cases;
  suppose
    c in dom f;
    hence thesis by A1,Def7;
  end;
  suppose
A2: not c in dom f;
    hence f".c = 0 qua Complex" by A1,FUNCT_1:def 2
      .= (f.c)" by A2,FUNCT_1:def 2;
  end;
end;

registration
  let f be real-valued Function;
  cluster f" -> real-valued;
  coherence
  proof
    let x be object;
    assume x in dom (f");
    then f".x = (f.x)" by Def7;
    hence thesis;
  end;
end;

registration
  let f be RAT-valued Function;
  cluster f" -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng (f");
    then consider x being object such that
A1: x in dom (f") and
A2: (f").x = y by FUNCT_1:def 3;
    f".x = (f.x)" by A1,Def7;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  redefine func f" -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f") = dom f & rng (f") c= COMPLEX by Def7,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  redefine func f" -> PartFunc of C,REAL;
  coherence
  proof
    dom (f") = dom f & rng (f") c= REAL by Def7,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  redefine func f" -> PartFunc of C,RAT;
  coherence
  proof
    dom (f") = dom f & rng (f") c= RAT by Def7,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  cluster f" -> total for PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f") = dom f by Def7
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  cluster f" -> total for PartFunc of C,REAL;
  coherence
  proof
    dom (f") = dom f by Def7
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  cluster f" -> total for PartFunc of C,RAT;
  coherence
  proof
    dom (f") = dom f by Def7
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let f be complex-valued FinSequence;
  cluster f" -> FinSequence-like;
  coherence
  proof
    dom (f") = dom f by Def7;
    hence thesis by Lm1;
  end;
end;

begin :: f^2

definition
  let f be complex-valued Function;
  func f^2 -> Function equals
  f (#) f;
  coherence;
end;

theorem Th11:
  for f being complex-valued Function holds dom (f^2) = dom f &
  for c being object holds f^2.c = (f.c)^2
proof
  let f be complex-valued Function;
  thus
A1: dom (f^2) = dom f /\ dom f by Def4
    .= dom f;
  let c be object;
  per cases;
  suppose
    c in dom f;
    hence thesis by A1,Def4;
  end;
  suppose
A2: not c in dom f;
    hence f^2.c = 0 qua Complex^2 by A1,FUNCT_1:def 2
      .= (f.c)^2 by A2,FUNCT_1:def 2;
  end;
end;

registration
  let f be complex-valued Function;
  cluster f^2 -> complex-valued;
  coherence;
end;

registration
  let f be real-valued Function;
  cluster f^2 -> real-valued;
  coherence;
end;

registration
  let f be RAT-valued Function;
  cluster f^2 -> RAT-valued;
  coherence;
end;

registration
  let f be INT-valued Function;
  cluster f^2 -> INT-valued;
  coherence;
end;

registration
  let f be natural-valued Function;
  cluster f^2 -> natural-valued;
  coherence;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  redefine func f^2 -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f^2) = dom f & rng (f^2) c= COMPLEX by Th11,VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be real-membered set;
  let f be PartFunc of C,D;
  redefine func f^2 -> PartFunc of C,REAL;
  coherence
  proof
    dom (f^2) = dom f & rng (f^2) c= REAL by Th11,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  redefine func f^2 -> PartFunc of C,RAT;
  coherence
  proof
    dom (f^2) = dom f & rng (f^2) c= RAT by Th11,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  redefine func f^2 -> PartFunc of C,INT;
  coherence
  proof
    dom (f^2) = dom f & rng (f^2) c= INT by Th11,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be natural-membered set;
  let f be PartFunc of C,D;
  redefine func f^2 -> PartFunc of C,NAT;
  coherence
  proof
    dom (f^2) = dom f & rng (f^2) c= NAT by Th11,VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  cluster f^2 -> total for PartFunc of C,COMPLEX;
  coherence;
end;

registration
  let C be set;
  let D be real-membered non empty set;
  let f be Function of C,D;
  cluster f^2 -> total for PartFunc of C,REAL;
  coherence;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  cluster f^2 -> total for PartFunc of C,RAT;
  coherence;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  cluster f^2 -> total for PartFunc of C,INT;
  coherence;
end;

registration
  let C be set;
  let D be natural-membered non empty set;
  let f be Function of C,D;
  cluster f^2 -> total for PartFunc of C,NAT;
  coherence;
end;

registration
  let f be complex-valued FinSequence;
  cluster f^2 -> FinSequence-like;
  coherence;
end;

begin :: f1 - f2

definition
  let f1,f2 be complex-valued Function;
  func f1 - f2 -> Function equals
  f1 + - f2;
  coherence;
end;

registration
  let f1,f2 be complex-valued Function;
  cluster f1-f2 -> complex-valued;
  coherence;
end;

registration
  let f1,f2 be real-valued Function;
  cluster f1-f2 -> real-valued;
  coherence;
end;

registration
  let f1,f2 be RAT-valued Function;
  cluster f1-f2 -> RAT-valued;
  coherence;
end;

registration
  let f1,f2 be INT-valued Function;
  cluster f1-f2 -> INT-valued;
  coherence;
end;

theorem Th12:
  for f1,f2 being complex-valued Function holds dom (f1-f2) = dom
  f1 /\ dom f2
proof
  let f1,f2 be complex-valued Function;
  thus dom (f1-f2) = dom f1 /\ dom -f2 by Def1
    .= dom f1 /\ dom f2 by Def5;
end;

theorem
  for f1,f2 being complex-valued Function
for c being object st c in dom (f1-f2) holds (f1-f2).c = f1.c - f2.c
proof
  let f1,f2 be complex-valued Function;
  let c be object;
  assume c in dom (f1-f2);
  hence (f1-f2).c = f1.c+(-f2).c by Def1
    .= f1.c-f2.c by Th8;
end;

theorem
  for f1,f2 being complex-valued Function, f being Function st dom f =
  dom (f1-f2) & for c being object st c in dom f holds f.c = f1.c - f2.c
   holds f = f1-f2
proof
  let f1,f2 be complex-valued Function, f be Function such that
A1: dom f = dom (f1-f2) and
A2: for c being object st c in dom f holds f.c = f1.c - f2.c;
  thus dom f = dom (f1-f2) by A1;
  let c be object;
  assume
A3: c in dom f;
  hence f.c = f1.c - f2.c by A2
    .= f1.c+(-f2).c by Th8
    .= (f1-f2).c by A1,A3,Def1;
end;

definition
  let C be set;
  let D1,D2 be complex-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1-f2 -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= COMPLEX by Th12,
VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be real-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1-f2 -> PartFunc of C,REAL;
  coherence
  proof
    dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= REAL by Th12,VALUED_0:def 3
;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be rational-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1-f2 -> PartFunc of C,RAT;
  coherence
  proof
    dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= RAT by Th12,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be integer-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1-f2 -> PartFunc of C,INT;
  coherence
  proof
    dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= INT by Th12,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

Lm3: for C being set, D1,D2 being complex-membered non empty set, f1 being
Function of C,D1, f2 being Function of C,D2 holds dom(f1-f2) = C

proof
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  thus dom(f1-f2) = dom f1 /\ dom -f2 by Def1
    .= C /\ dom -f2 by FUNCT_2:def 1
    .= C /\ C by FUNCT_2:def 1
    .= C;
end;

registration
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1-f2 -> total for PartFunc of C,COMPLEX;
  coherence
  by Lm3,PARTFUN1:def 2;
end;

registration
  let C be set;
  let D1,D2 be real-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1-f2 -> total for PartFunc of C,REAL;
  coherence
  by Lm3,PARTFUN1:def 2;
end;

registration
  let C be set;
  let D1,D2 be rational-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1-f2 -> total for PartFunc of C,RAT;
  coherence
  by Lm3,PARTFUN1:def 2;
end;

registration
  let C be set;
  let D1,D2 be integer-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1-f2 -> total for PartFunc of C,INT;
  coherence
  by Lm3,PARTFUN1:def 2;
end;

theorem
  for C being set, D1,D2 being complex-membered non empty set for f1
  being Function of C,D1, f2 being Function of C,D2 for c being Element of C
  holds (f1-f2).c = f1.c - f2.c
proof
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1, f2 be Function of C,D2;
  let c be Element of C;
A1: dom(f1-f2) = C by FUNCT_2:def 1;
  per cases;
  suppose
    C is non empty;
    hence (f1-f2).c = f1.c + (-f2).c by A1,Def1
      .= f1.c - f2.c by Th8;
  end;
  suppose
A2: C is empty;
    then f2.c = 0;
    hence thesis by A2;
  end;
end;

registration
  let f1, f2 be complex-valued FinSequence;
  cluster f1-f2 -> FinSequence-like;
  coherence;
end;

begin :: f1 /" f2

definition
  let f1,f2 be complex-valued Function;
  func f1 /" f2 -> Function equals
  f1 (#) (f2");
  coherence;
end;

theorem Th16:
  for f1,f2 being complex-valued Function holds dom (f1/"f2) = dom
  f1 /\ dom f2
proof
  let f1,f2 be complex-valued Function;
  thus dom (f1/"f2) = dom f1 /\ dom (f2") by Def4
    .= dom f1 /\ dom f2 by Def7;
end;

theorem
  for f1,f2 being complex-valued Function
   for c being object holds (f1/"f2).c = f1.c / f2.c
proof
  let f1,f2 be complex-valued Function;
  let c be object;
A1: dom (f1/"f2) = dom f1 /\ dom f2 by Th16;
  per cases;
  suppose
    c in dom (f1/"f2);
    hence (f1/"f2).c = f1.c * (f2").c by Def4
      .= f1.c / f2.c by Th10;
  end;
  suppose
A2: not c in dom (f1/"f2);
    then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4;
    then
A3: f1.c = 0 or f2.c = 0 by FUNCT_1:def 2;
    thus (f1/"f2).c = 0 / 0 by A2,FUNCT_1:def 2
      .= f1.c / f2.c by A3;
  end;
end;

registration
  let f1,f2 be complex-valued Function;
  cluster f1/"f2 -> complex-valued;
  coherence;
end;

registration
  let f1,f2 be real-valued Function;
  cluster f1/"f2 -> real-valued;
  coherence;
end;

registration
  let f1,f2 be RAT-valued Function;
  cluster f1/"f2 -> RAT-valued;
  coherence;
end;

definition
  let C be set;
  let D1,D2 be complex-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1/"f2 -> PartFunc of C,COMPLEX;
  coherence
  proof
    dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= COMPLEX by Th16,
VALUED_0:def 1;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be real-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1/"f2 -> PartFunc of C,REAL;
  coherence
  proof
    dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= REAL by Th16,
VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D1,D2 be rational-membered set;
  let f1 be PartFunc of C,D1;
  let f2 be PartFunc of C,D2;
  redefine func f1/"f2 -> PartFunc of C,RAT;
  coherence
  proof
    dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= RAT by Th16,
RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

Lm4: for C being set, D1,D2 being complex-membered non empty set for f1 being
Function of C,D1, f2 being Function of C,D2 holds dom(f1/"f2) = C

proof
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1, f2 be Function of C,D2;
  thus dom(f1/"f2) = dom f1 /\ dom f2 by Th16
    .= C /\ dom f2 by FUNCT_2:def 1
    .= C /\ C by FUNCT_2:def 1
    .= C;
end;

registration
  let C be set;
  let D1,D2 be complex-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1/"f2 -> total for PartFunc of C,COMPLEX;
  coherence
  by Lm4,PARTFUN1:def 2;
end;

registration
  let C be set;
  let D1,D2 be real-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1/"f2 -> total for PartFunc of C,REAL;
  coherence
  by Lm4,PARTFUN1:def 2;
end;

registration
  let C be set;
  let D1,D2 be rational-membered non empty set;
  let f1 be Function of C,D1;
  let f2 be Function of C,D2;
  cluster f1/"f2 -> total for PartFunc of C,RAT;
  coherence
  by Lm4,PARTFUN1:def 2;
end;

registration
  let f1, f2 be complex-valued FinSequence;
  cluster f1/"f2 -> FinSequence-like;
  coherence;
end;

begin :: abs f

definition
  let f be complex-valued Function;
  deffunc F(object) = |.f.$1.|;
  func |. f .| -> real-valued Function means
  :Def11:
  dom it = dom f & for c
  being object st c in dom it holds it.c = |. f.c .|;
  existence
  proof
    consider g being Function such that
A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x)
    from FUNCT_1:sch 3;
    g is real-valued
    proof
      let x be object;
      assume x in dom g;
      then g.x = |. f.x .| by A1;
      hence thesis;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let h, g be real-valued Function such that
A2: dom h = dom f and
A3: for c being object st c in dom h holds h.c = F(c) and
A4: dom g = dom f and
A5: for c being object st c in dom g holds g.c = F(c);
    now
      let x be object;
      assume
A6:   x in dom h;
      hence h.x = F(x) by A3
        .= g.x by A2,A4,A5,A6;
    end;
    hence thesis by A2,A4;
  end;
  projectivity
  proof
    let r be real-valued Function;
    let h be complex-valued Function;
    assume that
    dom r = dom h and
A7: for c being object st c in dom r holds r.c = |.h.c.|;
    thus dom r = dom r;
    let c be object;
    assume
A8: c in dom r;
    hence r.c = |.|.h.c.|.| by A7
      .= |.r.c.| by A7,A8;
  end;
end;

notation
  let f be complex-valued Function;
  synonym abs f for |. f .|;
end;

theorem
  for f being complex-valued Function
   for c being object holds |.f.|.c = |.f.c.|
proof
  let f be complex-valued Function;
  let c be object;
A1: dom |.f.| = dom f by Def11;
  per cases;
  suppose
    c in dom f;
    hence thesis by A1,Def11;
  end;
  suppose
A2: not c in dom f;
    hence |.f.|.c = |.0 qua Complex.| by A1,COMPLEX1:44,FUNCT_1:def 2
      .= |.f.c.| by A2,FUNCT_1:def 2;
  end;
end;

registration
  let f be RAT-valued Function;
  cluster |.f.| -> RAT-valued;
  coherence
  proof
    let y be object;
    assume y in rng |.f.|;
    then consider x being object such that
A1: x in dom |.f.| and
A2: (|.f.|).x = y by FUNCT_1:def 3;
    |.f.|.x = |.f.x.| by A1,Def11;
    hence thesis by A2,RAT_1:def 2;
  end;
end;

registration
  let f be INT-valued Function;
  cluster |.f.| -> natural-valued;
  coherence
  proof
    let x be object;
     |.f.x.| is natural;
    hence thesis by Def11;
  end;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  redefine func |.f.| -> PartFunc of C,REAL;
  coherence
  proof
    dom |.f.| = dom f & rng |.f.| c= REAL by Def11,VALUED_0:def 3;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be complex-membered set;
  let f be PartFunc of C,D;
  redefine func abs(f) -> PartFunc of C,REAL;
  coherence
  proof
    abs(f) = |.f.|;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  redefine func |.f.| -> PartFunc of C,RAT;
  coherence
  proof
    dom |.f.| = dom f & rng |.f.| c= RAT by Def11,RELAT_1:def 19;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be rational-membered set;
  let f be PartFunc of C,D;
  redefine func abs(f) -> PartFunc of C,RAT;
  coherence
  proof
    abs(f) = |.f.|;
    hence thesis;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  redefine func |.f.| -> PartFunc of C,NAT;
  coherence
  proof
    dom |.f.| = dom f & rng |.f.| c= NAT by Def11,VALUED_0:def 6;
    hence thesis by RELSET_1:4;
  end;
end;

definition
  let C be set;
  let D be integer-membered set;
  let f be PartFunc of C,D;
  redefine func abs(f) -> PartFunc of C,NAT;
  coherence
  proof
    abs(f) = |.f.|;
    hence thesis;
  end;
end;

registration
  let C be set;
  let D be complex-membered non empty set;
  let f be Function of C,D;
  cluster |.f.| -> total for PartFunc of C,REAL;
  coherence
  proof
    dom |.f.| = dom f by Def11
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be rational-membered non empty set;
  let f be Function of C,D;
  cluster |.f.| -> total for PartFunc of C,RAT;
  coherence
  proof
    dom |.f.| = dom f by Def11
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let C be set;
  let D be integer-membered non empty set;
  let f be Function of C,D;
  cluster |.f.| -> total for PartFunc of C,NAT;
  coherence
  proof
    dom |.f.| = dom f by Def11
      .= C by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

registration
  let f be complex-valued FinSequence;
  cluster |.f.| -> FinSequence-like;
  coherence
  proof
    dom abs f = dom f by Def11;
    hence thesis by Lm1;
  end;
end;

theorem
  for f, g being FinSequence, h being Function st dom h = dom f /\ dom g
  holds h is FinSequence by Lm2;

begin :: Addenda

:: from RELOC, 2008.02.14, A.T.

reserve m,j,p,q,n,l for Element of NAT;

definition
  let p be Function, k be Nat;
  func Shift(p,k) -> Function means
  :Def12:
  dom it = { m+k where m is Nat:m in dom p } &
  for m being Nat st m in dom p holds it.(m+k) = p.m;
  existence
  proof
    defpred P[object,object] means ex m being Nat st $1 = m+k & $2 = p.m;
    set A = { m+k where m is Nat:m in dom p };
A1: for e being object st e in A ex u being object st P[e,u]
    proof
      let e be object;
      assume e in A;
      then consider m being Nat such that
A2:   e = m+k and
      m in dom p;
      take p.m;
      thus thesis by A2;
    end;
    consider f being Function such that
A3: dom f = A and
A4: for e being object st e in A holds P[e,f.e] from CLASSES1:sch 1(A1);
    take f;
    thus dom f = { m+k where m is Nat :m in dom p } by A3;
    let m be Nat;
    assume m in dom p;
    then m+k in A;
    then ex j being Nat st m+k = j+k & f.(m+k) = p.j by A4;
    hence thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be Function such that
A5: dom IT1 = { m+k where m is Nat:m in dom p } and
A6: for m being Nat st m in dom p holds IT1.(m+k) = p.m and
A7: dom IT2 = { m+k where m is Nat:m in dom p } and
A8: for m being Nat st m in dom p holds IT2.(m+k) = p.m;
    for x being object st x in dom IT1 holds IT1.x = IT2.x
    proof
      let x be object;
      assume x in dom IT1;
      then consider m being Nat such that
A9:   x = m+k & m in dom p by A5;
      thus IT1.x = p.m by A6,A9
        .= IT2.x by A8,A9;
    end;
    hence thesis by A5,A7;
  end;
end;

registration
  let p be Function, k be Nat;
  cluster Shift(p,k) -> NAT-defined;
  coherence
  proof
A1: dom Shift(p,k) = { m+k where m is Nat:m in dom p } by Def12;
    Shift(p,k) is NAT-defined
    proof
      let x be object;
      assume x in dom Shift(p,k);
      then ex m being Nat st x = m+k & m in dom p by A1;
      hence thesis by ORDINAL1:def 12;
    end;
    hence thesis;
  end;
end;

theorem :: SCMFSA8C:11
  for P,Q being Function, k being Nat st P c= Q holds Shift(P
  ,k) c= Shift(Q,k)
proof
  let P,Q be Function;
  let k be Nat;
  assume
A1: P c= Q;
  then
A2: dom P c= dom Q by GRFUNC_1:2;
A3: dom Shift(P,k) = {m + k where m is Nat: m in dom P} by Def12;
A4: dom Shift(Q,k) = {m + k where m is Nat: m in dom Q} by Def12;
A5: now
    let x be object;
    assume x in dom Shift(P,k);
    then ex m1 being Nat st x = m1 + k & m1 in dom P by A3;
    hence x in dom Shift(Q,k) by A2,A4;
  end;
  now
    let x be object;
    assume x in dom Shift(P,k);
    then consider m1 being Nat such that
A6: x = m1 + k and
A7: m1 in dom P by A3;
    thus Shift(P,k).x = Shift(P,k).(m1 + k) by A6
      .= P.m1 by A7,Def12
      .= Q.m1 by A1,A7,GRFUNC_1:2
      .= Shift(Q,k).(m1 + k) by A2,A7,Def12
      .= Shift(Q,k).x by A6;
  end;
  hence thesis by A5,GRFUNC_1:2,TARSKI:def 3;
end;

theorem :: SCMFSA_4:32
  for n,m being Nat
  for I being Function holds Shift(Shift(I,m),n) = Shift(I,m+n)
proof let n,m be Nat;
  let I be Function;
  set A = {l+m where l is Nat:l in dom I };
A1: dom Shift(I,m) = A by Def12;
A2: now
    let l be Nat;
    assume
A3: l in dom I;
    then
A4: l+m in dom Shift(I,m) by A1;
    thus Shift(Shift(I,m),n).(l+(m+n)) = Shift(Shift(I,m),n).(l+m+n)
      .= Shift(I,m).(l+m) by A4,Def12
      .= I.l by A3,Def12;
  end;
  {p+n where p is Nat: p in A } = { q+(m+n) where q is Nat: q in dom I}
  proof
    thus {p+n where p is Nat: p in A } c= { q+(m+n) where q is Nat: q in dom I}
    proof
      let x be object;
      assume x in {p+n where p is Nat: p in A };
      then consider p being Nat such that
A5:   x = p+n and
A6:   p in A;
      consider l being Nat such that
A7:   p = l+m and
A8:   l in dom I by A6;
      x = l+(m+n) by A5,A7;
      hence thesis by A8;
    end;
    let x be object;
    assume x in { q+(m+n) where q is Nat: q in dom I};
    then consider q being Nat such that
A9: x = q+(m+n) & q in dom I;
    x = (q+m)+n & q+m in A by A9;
    hence thesis;
  end;
  then dom Shift(Shift(I,m),n) =
   { l+(m+n) where l is Nat: l in dom I} by A1,Def12;
  hence thesis by A2,Def12;
end;

theorem :: SCMFSA_4:33
  for s,f be Function for n being Nat holds Shift(f*s,n) = f*Shift(s,n)
proof
  let s,f be Function;
  let n be Nat;
A1: dom(f*s) c= dom s by RELAT_1:25;
A2: dom Shift(s,n)= { m+n where m is Nat: m in dom s } by Def12;
  now
    let e be object;
    thus e in { m+n where m is Nat: m in dom(f*s) }
      implies e in dom Shift(s,n) & Shift(s,n).
    e in dom f
    proof
      assume e in { m+n where m is Nat: m in dom(f*s) };
      then consider m being Nat such that
A3:   e = m+n and
A4:   m in dom(f*s);
      thus e in dom Shift(s,n) by A2,A1,A3,A4;
      Shift(s,n).e = s.m by A1,A3,A4,Def12;
      hence thesis by A4,FUNCT_1:11;
    end;
    assume e in dom Shift(s,n);
    then consider m0 being Nat such that
A5: e = m0+n and
A6: m0 in dom s by A2;
    assume Shift(s,n).e in dom f;
    then s.m0 in dom f by A5,A6,Def12;
    then m0 in dom(f*s) by A6,FUNCT_1:11;
    hence e in { m+n where m is Nat: m in dom(f*s) } by A5;
  end;
  then Shift(s,n)"dom f = { m+n where m is Nat: m in dom(f*s) }
          by FUNCT_1:def 7;
  then
A7: dom(f*Shift(s,n)) = { m+n where m is Nat: m in dom(f*s) } by RELAT_1:147;
  now
    let m be Nat;
    assume
A8: m in dom(f*s);
    then m+n in dom Shift(s,n) by A2,A1;
    hence (f*Shift(s,n)).(m+n) = f.(Shift(s,n).(m+n)) by FUNCT_1:13
      .= f.(s.m) by A1,A8,Def12
      .= (f*s).m by A8,FUNCT_1:12;
  end;
  hence thesis by A7,Def12;
end;

theorem :: SCMFSA_4:34
  for I,J being Function, n being Nat
   holds Shift(I +* J, n) = Shift(I,n) +* Shift(J,n)
proof
  let I,J be Function, n be Nat;
A1: dom Shift(J,n) = { m+n where m is Nat: m in dom J } by Def12;
A2: now
    let m be Nat such that
A3: m in dom(I +* J);
    per cases;
    suppose
A4:   m in dom J;
      then m+n in dom Shift(J,n) by A1;
      hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(J,n).(m+n) by FUNCT_4:13
        .= J.m by A4,Def12
        .= (I +* J).m by A4,FUNCT_4:13;
    end;
    suppose
A5:   not m in dom J;
      m in dom I \/ dom J by A3,FUNCT_4:def 1;
      then
A6:   m in dom I by A5,XBOOLE_0:def 3;
      not ex l being Nat st m+n = l+n & l in dom J by A5;
      then not m+n in dom Shift(J,n) by A1;
      hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(I,n).(m+n) by FUNCT_4:11
        .= I.m by A6,Def12
        .= (I +* J).m by A5,FUNCT_4:11;
    end;
  end;
A7: dom Shift(I,n) = { m+n where m is Nat: m in dom I } by Def12;
A8: dom Shift(I,n) \/ dom Shift(J,n)
          = { m+n where m is Nat: m in dom I \/ dom J }
  proof
    hereby
      let x be object;
      assume x in dom Shift(I,n) \/ dom Shift(J,n);
      then x in dom Shift(I,n) or x in dom Shift(J,n) by XBOOLE_0:def 3;
      then consider m being Nat such that
A9:   x = m+n & m in dom J or x = m+n & m in dom I by A1,A7;
      m in dom I \/ dom J by A9,XBOOLE_0:def 3;
      hence x in { l+n where l is Nat: l in dom I \/ dom J } by A9;
    end;
    let x be object;
    assume x in { m+n where m is Nat: m in dom I \/ dom J };
    then consider m being Nat such that
A10: x = m+n and
A11: m in dom I \/ dom J;
    m in dom I or m in dom J by A11,XBOOLE_0:def 3;
    then x in dom Shift(I,n) or x in dom Shift(J,n) by A1,A7,A10;
    hence thesis by XBOOLE_0:def 3;
  end;
  dom(I +* J) = dom I \/ dom J by FUNCT_4:def 1;
  then dom(Shift(I,n) +* Shift(J,n)) =
   { m+n where m is Nat: m in dom(I +* J ) } by A8,FUNCT_4:def 1;
  hence thesis by A2,Def12;
end;

:: from SCMPDS_4, 2008.03.16, A.T.

theorem Th24:
  for p being Function,k,il being Nat st il in dom p
  holds il+k in dom Shift(p,k)
proof
  let p be Function, k,il be Nat such that
A1: il in dom p;
  dom Shift(p,k) = { loc+k where loc is Nat : loc in dom p} by Def12;
  hence thesis by A1;
end;

:: missing, 2008.03.16, A.T.

theorem Th25:
  for p being Function, k being Nat holds rng Shift(p,k) c= rng p
proof
  let p be Function, k being Nat;
  let y be object;
  assume y in rng Shift(p,k);
  then consider x being object such that
A1: x in dom Shift(p,k) and
A2: y = Shift(p,k).x by FUNCT_1:def 3;
  x in { m+k where m is Nat:m in dom p } by A1,Def12;
  then consider m being Nat such that
A3: x = m+k and
A4: m in dom p;
  p.m = Shift(p,k).x by A3,A4,Def12;
  hence thesis by A2,A4,FUNCT_1:def 3;
end;

theorem
  for p being Function st dom p c= NAT for k being Nat holds
  rng Shift(p,k) = rng p
proof
  let p be Function such that
A1: dom p c= NAT;
  let k be Nat;
  thus rng Shift(p,k) c= rng p by Th25;
  let y be object;
  assume y in rng p;
  then consider x being object such that
A2: x in dom p and
A3: y = p.x by FUNCT_1:def 3;
  reconsider x as Element of NAT by A1,A2;
  x+k in dom Shift(p,k) & Shift(p,k).(x+k) = y by A2,A3,Def12,Th24;
  hence thesis by FUNCT_1:def 3;
end;

registration
  let p be finite Function, k be Nat;
  cluster Shift(p,k) -> finite;
  coherence
  proof
    deffunc F(Nat) = $1+k;
A1: dom p is finite;
A2: { F(w) where w is Element of NAT: w in dom p } is finite
          from FRAENKEL:sch 21(A1);
     dom Shift(p,k) c= { F(w) where w is Element of NAT: w in dom p }
    proof
     let e be object;
     assume e in dom Shift(p,k);
      then e in { F(i) where i is Nat: i in dom p } by Def12;
      then consider i being Nat such that
A3:    e = F(i) & i in dom p;
     reconsider i as Element of NAT by ORDINAL1:def 12;
      e = F(i) & i in dom p by A3;
     hence e in { F(w) where w is Element of NAT: w in dom p };
    end;
    hence thesis by A2,FINSET_1:10;
  end;
end;

reserve e1,e2 for ExtReal;

definition
  let X be non empty ext-real-membered set, s be sequence of X;
  redefine attr s is increasing means
  for n being Nat holds s.n < s.(n+1);
  compatibility
  proof
    thus s is increasing implies for n being Nat holds s.n < s.(n+1 )
    proof
      assume
A1:   s is increasing;
      let n be Nat;
A2:   n < n+1 by NAT_1:13;
      dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
      hence thesis by A1,A2;
    end;
    assume
A3: for n being Nat holds s.n < s.(n+1);
    let e1,e2;
    assume e1 in dom s & e2 in dom s;
    then reconsider m=e1, n=e2 as Nat;
    defpred P[Nat] means m < $1 implies s.m < 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 m < j+1;
      then m <= j by NAT_1:13;
      then s.m < s.j or m = j by A5,XXREAL_0:1;
      hence thesis by A3,XXREAL_0:2;
    end;
    assume
A6: e1 < e2;
A7: P[0];
    for j being Nat holds P[j] from NAT_1:sch 2(A7,A4);
    then s.m < s.n by A6;
    hence thesis;
  end;
  redefine attr s is decreasing means
  for n being Nat holds s.n > s.(n+1);
  compatibility
  proof
    thus s is decreasing implies for n being Nat holds s.n > s.(n+1 )
    proof
      assume
A8:   s is decreasing;
      let n be Nat;
A9:   n < n+1 by NAT_1:13;
      dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
      hence thesis by A8,A9;
    end;
    assume
A10: for n being Nat holds s.n > s.(n+1);
    let e1,e2;
    assume e1 in dom s & e2 in dom s;
    then reconsider m=e1, n=e2 as Nat;
    defpred P[Nat] means m < $1 implies s.m > s.$1;
A11: for j being Nat st P[j] holds P[j+1]
    proof
      let j being Nat such that
A12:  P[j];
      assume m < j+1;
      then m <= j by NAT_1:13;
      then s.m > s.j or m = j by A12,XXREAL_0:1;
      hence thesis by A10,XXREAL_0:2;
    end;
    assume
A13: e1 < e2;
A14: P[0];
    for j being Nat holds P[j] from NAT_1:sch 2(A14,A11);
    then s.m > s.n by A13;
    hence thesis;
  end;
  redefine attr s is non-decreasing means
  for n being Nat holds s.n <= s.(n+1);
  compatibility
  proof
    thus s is non-decreasing implies for n being Nat holds s.n <= s.(n+1 )
    proof
      assume
A15:  s is non-decreasing;
      let n be Nat;
A16:  n < n+1 by NAT_1:13;
      dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
      hence thesis by A15,A16;
    end;
    assume
A17: for n being Nat holds s.n <= s.(n+1);
    let e1,e2;
    assume e1 in dom s & e2 in dom s;
    then reconsider m=e1, n=e2 as Nat;
    defpred P[Nat] means m <= $1 implies s.m <= s.$1;
A18: for j being Nat st P[j] holds P[j+1]
    proof
      let j being Nat such that
A19:  P[j];
      assume m <= j+1;
      then
A20:  m < j+1 or m = j+1 by XXREAL_0:1;
      s.j <= s.(j+1) by A17;
      hence thesis by A19,A20,NAT_1:13,XXREAL_0:2;
    end;
    assume
A21: e1 <= e2;
A22: P[0];
    for j being Nat holds P[j] from NAT_1:sch 2(A22,A18);
    then s.m <= s.n by A21;
    hence thesis;
  end;
  redefine attr s is non-increasing means
  for n being Nat holds s.n >= s.(n+1);
  compatibility
  proof
    thus s is non-increasing implies for n being Nat holds s.n >= s.(n+1 )
    proof
      assume
A23:  s is non-increasing;
      let n be Nat;
A24:  n < n+1 by NAT_1:13;
      dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
      hence thesis by A23,A24;
    end;
    assume
A25: for n being Nat holds s.n >= s.(n+1);
    let e1,e2;
    assume e1 in dom s & e2 in dom s;
    then reconsider m=e1, n=e2 as Nat;
    defpred P[Nat] means m <= $1 implies s.m >= s.$1;
A26: for j being Nat st P[j] holds P[j+1]
    proof
      let j being Nat such that
A27:  P[j];
      assume m <= j+1;
      then
A28:  m < j+1 or m = j+1 by XXREAL_0:1;
      s.j >= s.(j+1) by A25;
      hence thesis by A27,A28,NAT_1:13,XXREAL_0:2;
    end;
    assume
A29: e1 <= e2;
A30: P[0];
    for j being Nat holds P[j] from NAT_1:sch 2(A30,A26);
    then s.m >= s.n by A29;
    hence thesis;
  end;
end;

:: from KURATO_2, 2008.09.05, A.T.

scheme
  SubSeqChoice { X() -> non empty set, S() -> sequence of X(), P[set]} :
   ex S1 being subsequence of S() st for n being Element of NAT holds P[S1.n]
provided
A1: for n being Element of NAT ex m being Element of NAT st n <= m & P[S
().m]
proof
  defpred P1[set,set,set] means $3 in NAT & (for m,k being Element of NAT st m
  = $2 & k = $3 holds m < k & P[S().k]);
  consider n0 being Element of NAT such that
  0 <= n0 and
A2: P[S().n0] by A1;
A3: for n being Nat for x being set ex y being set st P1[n,x,y]
  proof
    let n be Nat, x be set;
    per cases;
    suppose
      x in NAT;
      then reconsider mx = x as Element of NAT;
      consider my being Element of NAT such that
A4:   mx + 1 <= my & P[S().my] by A1;
      take my;
      thus my in NAT;
      thus thesis by A4,NAT_1:13;
    end;
    suppose
A5:   not x in NAT;
      take 0;
      set y = 0;
      thus y in NAT;
      let m, k be Element of NAT;
      assume that
A6:   m = x and
      k = y;
      thus thesis by A5,A6;
    end;
  end;
  consider g being Function such that
A7: dom g = NAT and
A8: g.0 = n0 and
A9: for n being Nat holds P1[n,g.n,g.(n+1)] from RECDEF_1:
  sch 1(A3);
  rng g c= NAT
  proof
    defpred P[Nat] means g.$1 in NAT;
    let y be object;
    assume y in rng g;
    then consider x being object such that
A10: x in dom g and
A11: g.x = y by FUNCT_1:def 3;
    reconsider n = x as Element of NAT by A7,A10;
A12: for k being Nat holds P[k] implies P[k+1] by A9;
A13: P[0] by A8;
    for k being Nat holds P[k] from NAT_1:sch 2(A13,A12);
    then g.n in NAT;
    hence thesis by A11;
  end;
  then reconsider g as sequence of NAT by A7,FUNCT_2:2;
  g is increasing
  by A9;
  then reconsider g as increasing sequence of NAT;
  reconsider S1 = S() * g as sequence of X();
A14: dom S1 = NAT by FUNCT_2:def 1;
  reconsider S1 as subsequence of S();
  take S1;
  thus for n being Element of NAT holds P[S1.n]
  proof
    let n be Element of NAT;
    per cases;
    suppose
      n = 0;
      hence thesis by A2,A8,A14,FUNCT_1:12;
    end;
    suppose
      n <> 0;
      then n >= 0 qua Nat + 1 by NAT_1:13;
      then reconsider n9 = n-1 as Element of NAT by INT_1:5;
      reconsider k = g.(n9+1) as Element of NAT;
      for m,k being Element of NAT st m = g.n9 & k = g.(n9+1) holds P[S()
      .k] by A9;
      then P[S().k];
      hence thesis by A14,FUNCT_1:12;
    end;
  end;
end;

:: from AMISTD_2, 2010.02.05, A.T.

theorem
  for k being Nat
  for F being NAT-defined Function
  holds dom F,dom Shift(F,k) are_equipotent
proof
  let k be Nat;
  let F be NAT-defined Function;
  defpred P[object,object] means
  ex il being Element of NAT
   st $1 = il & $2 = k+il;
A1: for e being object st e in dom F ex u being object st P[e,u]
  proof
    let e be object;
    assume e in dom F;
    then reconsider e as Element of NAT;
    take k+e, e;
    thus thesis;
  end;
  consider f being Function such that
A2: dom f = dom F and
A3: for x being object st x in dom F holds P[x,f.x] from CLASSES1:sch 1(A1);
  take f;
  hereby
    let x1, x2 be object such that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f.x1 = f.x2;
    consider i1 being Element of NAT such that
A7: x1 = i1 and
A8: f.x1 = k+i1 by A2,A3,A4;
    consider i2 being Element of NAT such that
A9: x2 = i2 and
A10: f.x2 = k+i2 by A2,A3,A5;
    thus x1 = x2 by A7,A6,A8,A10,A9;
  end;
  thus dom f = dom F by A2;
A11: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
  hereby
    let y be object;
    assume y in rng f;
    then consider x being object such that
A12: x in dom f and
A13: f.x = y by FUNCT_1:def 3;
    consider il being Element of NAT such that
A14: x = il and
A15: f.x = k+il by A2,A3,A12;
   thus y in dom Shift(F,k) by A2,A11,A12,A13,A14,A15;
  end;
  let y be object;
  assume y in dom Shift(F,k);
  then consider m being Nat such that
A16: y = (m+k) and
A17: m in dom F by A11;
  consider il being Element of NAT such that
A18: m = il and
A19: f.m = k+il by A3,A17;
  thus thesis by A2,A16,A17,A18,A19,FUNCT_1:def 3;
end;

registration
 let F be NAT-defined Function;
 reduce Shift(F,0) to F;
 reducibility
proof
A1: dom F = { m+(0 qua Nat) where m is Nat: m in dom F }
  proof
    hereby
     let a be object;
     assume
A2:   a in dom F;
      then reconsider l=a as Element of NAT;
      a = (l qua Nat)+(0 qua Complex);
     hence a in { m+(0 qua Nat)
      where m is Nat: m in dom F } by A2;
    end;
    let a be object;
    assume
    a in { m+(0 qua Complex) where m is Nat: m in dom F };
    then ex m being Nat
     st a = m+(0 qua Complex) & m in dom F;
    hence thesis;
  end;
  for m being Nat st m in dom F holds F.(m+(0 qua Complex)) = F.m;
  hence thesis by A1,Def12;
end;
end;

registration
  let X be non empty set;
  let F be X-valued Function, k be Nat;
  cluster Shift(F,k) -> X-valued;
  coherence
  proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
    thus rng Shift(F,k) c= X
     proof let x be object;
      assume x in rng Shift(F,k);
       then consider y being object such that
A2:     y in dom Shift(F,k) and
A3:     x = Shift(F,k).y by FUNCT_1:def 3;
       consider m being Nat such that
A4:     y = (m+k) and
A5:     m in dom F by A2,A1;
       Shift(F,k).(m+k) = F.m by A5,Def12
            .= F/.m by A5,PARTFUN1:def 6;
      hence x in X by A3,A4;
     end;
  end;
end;

registration  :: move somewhere !!!
 cluster non empty NAT-defined for Function;
 existence
  proof
   take id NAT;
   thus thesis;
  end;
end;

registration
  let F be empty Function, k be Nat;
  cluster Shift(F,k) -> empty;
  coherence
  proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
    assume Shift(F,k) is non empty;
    then reconsider f = Shift(F,k) as non empty Function;
    dom f is non empty;
    then consider a being object such that
A2: a in dom Shift(F,k);
    ex m being Nat st a = (m+k) & m in dom F by A1,A2;
    hence thesis;
  end;
end;

registration
  let F be non empty NAT-defined Function, k be Nat;
  cluster Shift(F,k) -> non empty;
  coherence
  proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
    consider a being object such that
A2: a in dom F by XBOOLE_0:def 1;
    reconsider a as Element of NAT by A2;
    consider m being Nat such that
A3: a = m;
    reconsider m as Element of NAT by ORDINAL1:def 12;
    (m+k) in dom Shift(F,k) by A1,A2,A3;
    hence thesis;
  end;
end;

::$CT

theorem
  for F being Function, k being Nat st k > 0
  holds not 0 in dom Shift(F,k)
proof
  let F be Function, k be Nat such that
A1: k > 0 and
A2: 0 in dom Shift(F,k);
  dom Shift(F,k) = { m+k where m is Nat: m in dom F } by Def12;
  then ex m being Nat st 0 = m+k &  m in dom F by A2;
  hence contradiction by A1;
end;

registration
 cluster NAT-defined finite non empty for Function;
 existence
  proof
   take f = 0 .--> 0;
    dom f = {0} by FUNCOP_1:13;
   hence dom f c= NAT by ZFMISC_1:31;
   thus thesis;
  end;
end;

registration
  let F be NAT-defined Relation;
  cluster dom F -> natural-membered;
 coherence;
end;

definition
  let F be non empty NAT-defined finite Function;
  func LastLoc F -> Element of NAT equals
   max dom F;
 coherence by ORDINAL1:def 12;
end;

definition
  let F be non empty NAT-defined finite Function;
  func CutLastLoc F -> Function equals
  F \ ( LastLoc F .--> F.LastLoc F );
  coherence;
end;

registration
 let F be non empty NAT-defined finite Function;
 cluster CutLastLoc F -> NAT-defined finite;
 coherence;
end;

theorem
  for F being non empty NAT-defined finite Function holds
  LastLoc F in dom F by XXREAL_2:def 8;

theorem
  for F, G being non empty NAT-defined finite Function st F c= G holds
  LastLoc F <= LastLoc G by RELAT_1:11,XXREAL_2:59;

theorem
  for F being non empty NAT-defined finite Function, l being
  Element of NAT st l in dom F holds l <= LastLoc F by XXREAL_2:def 8;

definition
  let F be non empty NAT-defined Function;
  func FirstLoc F -> Element of NAT equals
   min dom F;
  coherence by ORDINAL1:def 12;
end;

theorem
  for F being non empty NAT-defined finite Function holds
  FirstLoc F in dom F by XXREAL_2:def 7;

theorem
  for F, G being non empty NAT-defined finite Function st F c= G holds
  FirstLoc G <= FirstLoc F by RELAT_1:11,XXREAL_2:60;

theorem
  for l1 being Element of NAT
  for F being non empty NAT-defined finite Function st l1 in dom
  F holds FirstLoc F <= l1 by XXREAL_2:def 7;

theorem Th35:
  for F being non empty NAT-defined finite Function
  holds dom CutLastLoc F = (dom F) \ {LastLoc F}
proof
  let F be non empty NAT-defined finite Function;
A1: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F} by FUNCOP_1:13;
  reconsider R = {[LastLoc F, F.LastLoc F]} as Relation;
A2: R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:82;
  then
A3: dom R = {LastLoc F} by FUNCOP_1:13;
  thus dom CutLastLoc F c= (dom F) \ {LastLoc F}
  proof
    let x be object;
    assume x in dom CutLastLoc F;
    then consider y being object such that
A4: [x,y] in F \ R by A2,XTUPLE_0:def 12;
A5: not [x,y] in R by A4,XBOOLE_0:def 5;
A6: x in dom F by A4,XTUPLE_0:def 12;
    per cases by A5,TARSKI:def 1;
    suppose x <> LastLoc F;
      then not x in dom R by A3,TARSKI:def 1;
      hence thesis by A1,A2,A6,XBOOLE_0:def 5;
    end;
    suppose
A7:   y <> F.LastLoc F;
      now
        assume x in dom R;
        then x = LastLoc F by A3,TARSKI:def 1;
        hence contradiction by A4,A7,FUNCT_1:1;
      end;
      hence thesis by A1,A2,A6,XBOOLE_0:def 5;
    end;
  end;
  thus thesis by A1,XTUPLE_0:25;
end;

theorem
  for F being non empty NAT-defined finite Function
  holds dom F = dom CutLastLoc F \/ {LastLoc F}
proof
  let F be non empty NAT-defined finite Function;
  LastLoc F in dom F by XXREAL_2:def 8;
  then
A1: {LastLoc F} c= dom F by ZFMISC_1:31;
  dom CutLastLoc F = (dom F) \ {LastLoc F} by Th35;
  hence thesis by A1,XBOOLE_1:45;
end;

registration
 cluster 1-element NAT-defined finite for Function;
 existence
  proof
   take 0 .--> 0;
   thus thesis;
  end;
end;

registration
  let F be 1-element NAT-defined finite Function;
  cluster CutLastLoc F -> empty;
  coherence
  proof
    LastLoc F in dom F by XXREAL_2:def 8;
    then
A1: [LastLoc F,F.LastLoc F] in F by FUNCT_1:def 2;
    assume not thesis;
    then consider a being object such that
A2: a in CutLastLoc F;
A3: a = [LastLoc F,F.LastLoc F] by A1,A2,ZFMISC_1:def 10;
    not a in LastLoc F .--> F.LastLoc F by A2,XBOOLE_0:def 5;
    then not a in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82;
    hence thesis by A3,TARSKI:def 1;
  end;
end;

theorem Th37:
  for F being non empty NAT-defined finite Function
  holds card CutLastLoc F = card F - 1
proof
  let F be non empty NAT-defined finite Function;
  LastLoc F .--> F.LastLoc F c= F
  proof
    let a, b be object;
    assume [a,b] in LastLoc F .--> F.LastLoc F;
    then [a,b] in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82;
    then
A1: [a,b] = [LastLoc F,F.LastLoc F] by TARSKI:def 1;
    LastLoc F in dom F by XXREAL_2:def 8;
    hence thesis by A1,FUNCT_1:def 2;
  end;
  hence card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F)
  by CARD_2:44
    .= card F - card {[LastLoc F,F.LastLoc F]} by FUNCT_4:82
    .= card F - 1 by CARD_1:30;
end;

begin :: 2011.04.20, A.T.

registration let X be set, f be X-defined complex-valued Function;
 cluster -f -> X-defined;
 coherence
  proof
A1:  dom -f = dom f by Def5;
   thus dom -f c= X by A1;
  end;
 cluster f" -> X-defined;
 coherence
  proof
A2:  dom(f") = dom f by Def7;
   thus dom(f") c= X by A2;
  end;
 cluster f^2 -> X-defined;
 coherence
  proof
A3:  dom(f^2) = dom f by Th11;
   thus dom(f^2) c= X by A3;
  end;
 cluster |.f.| -> X-defined;
 coherence
  proof
A4:  dom |.f.| = dom f by Def11;
   thus dom |.f.| c= X by A4;
  end;
end;

registration let X be set;
 cluster total for X-defined natural-valued Function;
 existence
  proof
   take the total PartFunc of X, NAT;
   thus thesis;
  end;
end;

registration let X be set,
   f be total X-defined complex-valued Function;
 cluster -f -> total;
 coherence
  proof
A1:  dom -f = dom f by Def5;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A1,PARTFUN1:def 2;
  end;
 cluster f" -> total;
 coherence
  proof
A2:  dom(f") = dom f by Def7;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A2,PARTFUN1:def 2;
  end;
 cluster f^2 -> total;
 coherence
  proof
A3:  dom(f^2) = dom f by Th11;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A3,PARTFUN1:def 2;
  end;
 cluster |.f.| -> total;
 coherence
  proof
A4:  dom |.f.| = dom f by Def11;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A4,PARTFUN1:def 2;
  end;
end;

registration
 let X be set, f be X-defined complex-valued Function,
     r be Complex;
 cluster r+f -> X-defined;
 coherence
  proof
A1:  dom(r+f) = dom f by Def2;
   thus dom(r+f) c= X by A1;
  end;
 cluster f-r -> X-defined;
 coherence;
 cluster r(#)f -> X-defined;
 coherence
  proof
A2:  dom(r(#)f) = dom f by Def5;
   thus dom(r(#)f) c= X by A2;
  end;
end;

registration let X be set,
   f be total X-defined complex-valued Function,
     r be Complex;
 cluster r+f -> total;
 coherence
  proof
A1:  dom(r+f) = dom f by Def2;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A1,PARTFUN1:def 2;
  end;
 cluster f-r -> total;
 coherence;
 cluster r(#)f -> total;
 coherence
  proof
A2:  dom(r(#)f) = dom f by Def5;
    dom f = X by PARTFUN1:def 2;
   hence thesis by A2,PARTFUN1:def 2;
  end;
end;

registration
 let X be set, f1 be complex-valued Function;
 let f2 be X-defined complex-valued Function;
 cluster f1 + f2 -> X-defined;
 coherence
  proof
A1:  dom(f1 + f2) = dom f1 /\ dom f2 by Def1;
   thus dom(f1 + f2) c= X by A1;
  end;
 cluster f1 - f2 -> X-defined;
 coherence;
 cluster f1(#)f2 -> X-defined;
 coherence
  proof
A2:  dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
   thus dom(f1(#)f2) c= X by A2;
  end;
 cluster f1/"f2 -> X-defined;
 coherence;
end;

registration let X be set;
 let f1,f2 be total X-defined complex-valued Function;
 cluster f1 + f2 -> total;
 coherence
  proof
A1:  dom(f1 + f2) = dom f1 /\ dom f2 by Def1;
    dom f1 = X & dom f2 = X by PARTFUN1:def 2;
   hence thesis by A1,PARTFUN1:def 2;
  end;
 cluster f1 - f2 -> total;
 coherence;
 cluster f1(#)f2 -> total;
 coherence
  proof
A2:  dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
    dom f1 = X & dom f2 = X by PARTFUN1:def 2;
   hence thesis by A2,PARTFUN1:def 2;
  end;
 cluster f1/"f2 -> total;
 coherence;
end;

registration let X be non empty set;
 let F be X-valued non empty NAT-defined finite Function;
 cluster CutLastLoc F -> X-valued;
 coherence;
end;

theorem
 for f being Function
 for i,n being Nat st i in dom Shift(f,n)
  ex j being Nat st j in dom f & i = j + n
 proof let f be Function;
  let i,n be Nat;
A1: dom Shift(f,n) = { m+n where m is Nat:m in dom f } by Def12;
  assume i in dom Shift(f,n);
   then ex m being Nat st i = m + n & m in dom f by A1;
  hence ex j being Nat st j in dom f & i = j + n;
 end;

:: from PNPROC_1, 2012.02.20, A.T.

registration
  let p be FinSubsequence;
  let i be Nat;
  cluster Shift(p,i) -> FinSubsequence-like;
  coherence
  proof
    set X = {k+i where k is Nat : k in dom p },
        f = Shift(p,i);
    consider K being Nat such that
A1: dom p c= Seg K by FINSEQ_1:def 12;
A2: dom f = X by Def12;
    X c= Seg (i+K)
    proof
      let x be object;
      assume x in X;
      then consider k being Nat such that
A3:   x = k+i and
A4:   k in dom p;
A5:   i+k >= k by NAT_1:11;
A6:  k >= 1 by A1,A4,FINSEQ_1:1;
A7:  k <= K by A1,A4,FINSEQ_1:1;
      i+k >= 1 by A5,A6,XXREAL_0:2;
     hence thesis by A3,A7,FINSEQ_1:1,XREAL_1:6;
    end;
   hence f is FinSubsequence-like by A2;
  end;
end;

reserve i for Nat,
        k,k1,k2,j1 for Element of NAT,
        x,x1,x2,y for set;

theorem Th39:
  for p being FinSequence
  holds  dom Shift(p,i) = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)}
proof
  let p be FinSequence;
A1: dom p = Seg len p by FINSEQ_1:def 3
    .= {k where k is Nat: 1 <= k & k <= len p};
  set X = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)};
A2: dom Shift(p,i) = {k1+i where k1 is Nat: k1 in dom p} by Def12;
  thus dom Shift(p,i) c= X
  proof
    let x be object;
    assume x in dom Shift(p,i);
    then consider k1 being Nat such that
A3: x = k1+i and
A4: k1 in dom p by A2;
    consider k being Nat such that
A5: k1 = k and
A6: 1 <= k and
A7: k <= len p by A1,A4;
A8: i+1 <= i+k by A6,XREAL_1:7;
    i+k <= i+(len p) by A7,XREAL_1:7;
    hence thesis by A3,A5,A8;
  end;
  let x be object;
  assume x in X;
  then consider j1 being Nat such that
A9: x = j1 and
A10: i+1 <= j1 and
A11: j1 <= i+(len p);
  i+(0 qua Nat) <= i+1 by XREAL_1:7;
  then consider k2 being Nat such that
A12: j1 = i+k2 by A10,NAT_1:10,XXREAL_0:2;
A13: 1 <= k2 by A10,A12,XREAL_1:6;
  k2 <= len p by A11,A12,XREAL_1:6;
  then k2 in dom p by A1,A13;
  hence thesis by A2,A9,A12;
end;

theorem Th40:
  for q being FinSubsequence ex ss being FinSubsequence st
  dom ss = dom q & rng ss = dom Shift(q,i) &
  (for k st k in dom q holds ss.k = i+k) & ss is one-to-one
proof
  let q be FinSubsequence;
  consider n being Nat such that
A1: dom q c= Seg n by FINSEQ_1:def 12;
  defpred P[object,object] means ex k st k = $1 & $2 = i+k;
A2: for x being object st x in dom q ex y being object st P[x,y]
  proof
    let x be object;
    assume x in dom q;
    then reconsider x as Element of NAT;
    take i+x;
    thus thesis;
  end;
  consider f being Function such that
A3: dom f = dom q and
A4: for x being object st x in dom q holds P[x, f.x] from CLASSES1:sch 1(A2);
  reconsider ss = f as FinSubsequence by A1,A3,FINSEQ_1:def 12;
A5: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A6: rng ss = dom Shift(q,i)
  proof
    thus rng ss c= dom Shift(q,i)
    proof
      let y be object;
      assume y in rng ss;
      then consider x being object such that
A7:   x in dom ss and
A8:   y = ss.x by FUNCT_1:def 3;
      ex k1 st ( k1 = x)&( ss.x = i+k1) by A3,A4,A7;
      hence thesis by A3,A5,A7,A8;
    end;
    let y be object;
    assume y in dom Shift(q,i);
    then consider k2 being Nat such that
A9: y = k2+i and
A10: k2 in dom q by A5;
    ex k3 being Element of NAT st ( k3 = k2)&( ss.k2 = i+k3)
    by A4,A10;
    hence thesis by A3,A9,A10,FUNCT_1:def 3;
  end;
A11: for k st k in dom q holds ss.k = i+k
  proof
    let k;
    assume k in dom q;
    then ex k1 st ( k1 = k)&( ss.k = i+k1) by A4;
    hence thesis;
  end;
  for x1,x2 being object
   st x1 in dom ss & x2 in dom ss & ss.x1 = ss.x2 holds x1 = x2
  proof
    let x1,x2 be object;
    assume that
A12: x1 in dom ss and
A13: x2 in dom ss and
A14: ss.x1 = ss.x2;
A15: ex k1 st ( k1 = x1)&( ss.x1 = i+k1) by A3,A4,A12;
    ex k2 st ( k2 = x2)&( ss.x2 = i+k2) by A3,A4,A13;
    hence thesis by A14,A15;
  end;
  then ss is one-to-one;
  hence thesis by A3,A6,A11;
end;

Lm5: for p being FinSequence holds ex fs being FinSequence st
dom fs = dom p & rng fs = dom Shift(p,i) &
(for k st k in dom p holds fs.k = i+k) & fs is one-to-one
proof
  let p be FinSequence;
  consider ss being FinSubsequence such that
A1: dom ss = dom p and
A2: rng ss = dom Shift(p,i) and
A3: for k st k in dom p holds ss.k = i+k and
A4: ss is one-to-one by Th40;
  dom ss = Seg len p by A1,FINSEQ_1:def 3;
  then reconsider fs = ss as FinSequence by FINSEQ_1:def 2;
  dom fs = dom p by A1;
  hence thesis by A2,A3,A4;
end;

theorem Th41:
  for q being FinSubsequence holds card q = card Shift(q,i)
proof
  let q be FinSubsequence;
  ex ss being FinSubsequence st ( dom ss = dom q)&( rng ss =
  dom Shift(q,i))&( for k st k in dom q holds ss.k = i+k)&( ss is one-to-one)
  by Th40;
  then
A1: dom q, dom Shift(q,i) are_equipotent;
A2: card dom q = card q by CARD_1:62;
  card dom Shift(q,i) = card Shift(q,i) by CARD_1:62;
  hence thesis by A1,A2,CARD_1:5;
end;

theorem Th42:
  for p being FinSequence holds dom p = dom Seq Shift(p,i)
proof
  let p be FinSequence;
A1: rng Sgm dom Shift(p,i) = dom Shift(p,i) by FINSEQ_1:50;
A2: dom p = Seg len p by FINSEQ_1:def 3;
A3: dom Sgm dom Shift(p,i) = Seg len Sgm dom Shift(p,i) by FINSEQ_1:def 3;
  ex k be Nat st ( dom Shift(p,i) c= Seg k) by FINSEQ_1:def 12;
  then
A4: len Sgm dom Shift(p,i) = card dom Shift(p,i) by FINSEQ_3:39;
  card dom Shift(p,i) = card Shift(p,i) by CARD_1:62;
  then card dom Shift(p,i) = len p by Th41;
  hence thesis by A1,A2,A3,A4,RELAT_1:27;
end;

theorem Th43:
  for p being FinSequence st k in dom p holds (Sgm dom Shift(p,i)).k = i + k
proof
  let p be FinSequence;
  assume
A1: k in dom p;
  consider fs being FinSequence such that
A2: dom fs = dom p and
A3: rng fs = dom Shift(p,i) and
A4: for j st j in dom p holds fs.j = i+j
  and fs is one-to-one by Lm5;
A5: ex l be Nat st ( dom Shift(p,i) c= Seg l) by FINSEQ_1:def 12;
  reconsider fs as FinSequence of NAT by A3,FINSEQ_1:def 4;
  for n,m,k1,k2 being Nat st 1 <= n & n < m & m <= len fs &
  k1 = fs.n & k2 = fs.m holds k1 < k2
  proof
    let n,m,k1,k2 be Nat;
    assume that
A6: 1 <= n and
A7: n < m and
A8: m <= len fs and
A9: k1 = fs.n and
A10: k2 = fs.m;
    reconsider n,m as Element of NAT by ORDINAL1:def 12;
A11: dom fs = Seg len fs by FINSEQ_1:def 3
      .= {n1 where n1 is Nat: 1 <= n1 & n1 <= len fs};
    n+1 <= m by A7,INT_1:7;
    then n+1 <= len fs by A8,XXREAL_0:2;
    then
A12: n <= (len fs) - 1 by XREAL_1:19;
    (len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7;
    then (len fs) - 1 <= len fs by XREAL_1:20;
    then n <= len fs by A12,XXREAL_0:2;
    then
A13: n in dom p by A2,A6,A11;
    1 <= m by A6,A7,XXREAL_0:2;
    then
A14: m in dom p by A2,A8,A11;
A15: k1 = i+n by A4,A9,A13;
    k2 = i+m by A4,A10,A14;
    hence thesis by A7,A15,XREAL_1:8;
  end;
  then fs = Sgm dom Shift(p,i) by A3,A5,FINSEQ_1:def 13;
  hence thesis by A1,A4;
end;

theorem Th44:
  for p being FinSequence st k in dom p holds (Seq Shift(p,i)).k = p.k
proof
  let p be FinSequence;
  assume
A1: k in dom p;
  then
A2: k in dom Seq Shift(p,i) by Th42;
  (Shift(p,i)*(Sgm dom Shift(p,i))).k
  = Shift(p,i).((Sgm dom Shift(p,i)).k) by A2,FUNCT_1:12
    .= Shift(p,i).(i+k) by A1,Th43;
  hence thesis by A1,Def12;
end;

theorem
  for p being FinSequence holds Seq Shift(p,i) = p
proof
  let p be FinSequence;
A1: dom Seq Shift(p,i) = dom p by Th42;
  for x being object holds
   x in dom p implies (Seq Shift(p,i)).x = p.x by Th44;
  hence thesis by A1;
end;

reserve p1,p2 for FinSequence;

Lm6: for j,k,l being Nat st
1 <= j & j <= l or l+1 <= j & j <= l+k holds 1 <= j & j <= l+k
proof
  let j,k,l be Nat;
  assume that
A1: 1 <= j & j <= l or l+1 <= j & j <= l+k;
  per cases by A1;
  suppose
A2: 1 <= j & j <= l;
    l+(0 qua Nat) <= l+k by XREAL_1:7;
    hence thesis by A2,XXREAL_0:2;
  end;
  suppose
A3: l+1 <= j & j <= l+k;
    0 qua Nat+1 <= l+1 by XREAL_1:7;
    hence thesis by A3,XXREAL_0:2;
  end;
end;

theorem Th46:
  dom (p1 \/ Shift(p2,len p1)) = Seg (len p1 + len p2)
proof
A1: dom (p1 \/ Shift(p2,len p1)) = dom p1 \/ dom (Shift(p2,len p1))
    by XTUPLE_0:23;
A2: dom p1 = Seg len p1 by FINSEQ_1:def 3
      .= {k where k is Nat: 1 <= k & k <= len p1};
A3: dom (Shift(p2,len p1))
    = {k1 where k1 is Nat: len p1 + 1 <= k1 & k1 <= len p1 + len p2}
    by Th39;
    thus dom (p1 \/ Shift(p2,len p1)) c= Seg (len p1 + len p2)
    proof
      let x be object;
      assume x in dom (p1 \/ (Shift(p2,len p1)));
      then
A4:    x in dom p1 or x in dom (Shift(p2,len p1)) by A1,XBOOLE_0:def 3;
      then
A5:  ex k3 being Nat st x = k3 & 1 <= k3 & k3 <=
      len p1 or x = k3 & len p1 + 1 <= k3 & k3 <= len p1 + len p2 by A2,A3;
     reconsider x as Nat by A4;
A6:  1 <= x by A5,Lm6;
      x <= len p1 + len p2 by A5,Lm6;
      hence thesis by A6;
    end;
    let x be object;
    assume x in Seg (len p1 + len p2);
    then consider j being Nat such that
A7: x = j and
A8: 1 <= j and
A9: j <= len p1 + len p2;
    reconsider i0 = len p1 as Integer;
    1 <= j & j <= i0 or i0 + 1 <= j & j <= i0 + len p2 by A8,A9,INT_1:7;
    then x in dom p1 or x in dom Shift(p2,len p1) by A2,A3,A7;
    hence thesis by A1,XBOOLE_0:def 3;
end;

theorem Th47:
  for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds
  dom p1 misses dom Shift(p2,i)
proof
  let p1 be FinSequence, p2 be FinSubsequence;
  assume
A1: len p1 <= i;
A2: dom p1 = Seg len p1 by FINSEQ_1:def 3
    .= {k where k is Nat: 1 <= k & k <= len p1};
A3: dom Shift(p2,i) = {k+i where k is Nat: k in dom p2} by Def12;
  not ex x being object st x in dom p1 /\ dom Shift(p2,i)
  proof
    given x being object such that
A4: x in dom p1 /\ dom Shift(p2,i);
A5: x in dom p1 by A4,XBOOLE_0:def 4;
A6: x in dom Shift(p2,i) by A4,XBOOLE_0:def 4;
A7: ex k1 being Nat st ( x = k1)&( 1 <= k1)&( k1 <= len p1) by A2,A5;
    consider k2 being Nat such that
A8: x = k2+i and
A9: k2 in dom p2 by A3,A6;
    consider n being Nat such that
A10: dom p2 c= Seg n by FINSEQ_1:def 12;
A11: k2 in Seg n by A9,A10;
A12:  ex m being Nat st k2 = m & 1 <= m & m <= n by A11;
    reconsider x as Element of NAT by A4;
    len p1 + k2 <= i+k2 by A1,XREAL_1:7;
    then (len p1 + k2) - k2 < x - 0 by A8,A12,XREAL_1:15;
    hence contradiction by A7;
  end;
  hence dom p1 /\ dom Shift(p2,i) = {} by XBOOLE_0:def 1;
end;

theorem
  for p1,p2 being FinSequence holds p1^p2 = p1 \/ (Shift(p2,len p1))
proof
  let p1,p2;
A1: dom (p1 \/ (Shift(p2,len p1))) = Seg (len p1 + len p2) by Th46;
  dom p1 misses dom (Shift(p2,len p1)) by Th47;
  then reconsider p = p1 \/ (Shift(p2,len p1)) as FinSequence by A1,
FINSEQ_1:def 2,GRFUNC_1:13;
A2: dom p = Seg (len p1 + len p2) by Th46;
A3: for k be Nat st k in dom p1 holds p.k = p1.k
  proof
    let k be Nat;
    assume k in dom p1;
    then [k,p1.k] in p1 by FUNCT_1:def 2;
    then [k,p1.k] in p by XBOOLE_0:def 3;
    hence thesis by FUNCT_1:1;
  end;
  for k be Nat st k in dom p2 holds p.(len p1 + k) = p2.k
  proof
    let k be Nat;
    assume
A4: k in dom p2;
    dom (Shift(p2,len p1)) = {j+len p1 where j is Nat: j in dom p2} by Def12;
    then len p1 + k in dom (Shift(p2,len p1)) by A4;
    then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in
    (Shift(p2,len p1)) by FUNCT_1:def 2;
    then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in p
    by XBOOLE_0:def 3;
    then p.(len p1 + k) = (Shift(p2,len p1)).(len p1 + k) by FUNCT_1:1;
    hence thesis by A4,Def12;
  end;
  hence thesis by A2,A3,FINSEQ_1:def 7;
end;

theorem
  for p1 being FinSequence, p2 being FinSubsequence st i >= len p1
  holds p1 misses Shift(p2,i)
proof
  let p1 be FinSequence, p2 be FinSubsequence;
  assume i >= len p1;
  then dom p1 misses dom Shift(p2,i) by Th47;
  hence thesis by RELAT_1:179   ;
end;

theorem
 for F being total NAT-defined Function, p be NAT-defined Function,
     n be Element of NAT st Shift(p,n) c= F
 for i being Element of NAT st i in dom p holds F.(n+i) = p.i
 proof
  let F be total NAT-defined Function, p be NAT-defined Function,
     n be Element of NAT such that
A1: Shift(p,n) c= F;
  let i be Element of NAT;
  assume
A2: i in dom p;
   then n+i in dom Shift(p,n) by Th24;
  hence F.(n+i) = Shift(p,n).(n+i) by A1,GRFUNC_1:2
      .= p.i by A2,Def12;
 end;

theorem Th51:
  for p,q being FinSubsequence st q c= p holds Shift(q,i) c= Shift(p,i)
proof
  let p,q be FinSubsequence;
  assume
A1: q c= p;
A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12;
  let x,y be object;
  assume
A4: [x,y] in Shift(q,i);
  then
A5: x in dom Shift(q,i) by FUNCT_1:1;
A6: y = Shift(q,i).x by A4,FUNCT_1:1;
  consider k being Nat such that
A7: x = k+i and
A8: k in dom q by A2,A5;
A9: dom q c= dom p by A1,GRFUNC_1:2;
  then
A10: x in dom Shift(p,i) by A3,A7,A8;
  y = q.k by A6,A7,A8,Def12
    .= p.k by A1,A8,GRFUNC_1:2
    .= Shift(p,i).x by A7,A8,A9,Def12;
  hence thesis by A10,FUNCT_1:1;
end;

theorem
  for p1,p2 being FinSequence holds Shift(p2,len p1) c= p1^p2
proof
  let p1,p2 be FinSequence;
A1: dom Shift(p2,len p1) = {k+len p1 where k is Nat: k in dom p2} by Def12;
A2: dom Shift(p2,len p1) =
   {k where k is Nat: len p1 + 1 <= k & k <= len p1 + len p2}
    by Th39;
A3: dom (p1^p2) = Seg (len p1 + len p2) by FINSEQ_1:def 7
      .= {k where k is Nat: 1 <= k & k <= len p1 + len p2};
    let x,y be object;
    assume
A4: [x,y] in Shift(p2,len p1);
    then
A5: x in dom Shift(p2,len p1) by FUNCT_1:1;
A6: y = Shift(p2,len p1).x by A4,FUNCT_1:1;
    consider k being Nat such that
A7: x = k and
A8: len p1 + 1 <= k and
A9: k <= len p1 + len p2 by A2,A5;
    1 <= len p1 + 1 by INT_1:6;
    then 1 <= k by A8,XXREAL_0:2;
    then
A10: x in dom (p1^p2) by A3,A7,A9;
    consider j being Nat such that
A11: x = j+len p1 and
A12: j in dom p2 by A1,A5;
    y = p2.j by A6,A11,A12,Def12
      .= (p1^p2).x by A11,A12,FINSEQ_1:def 7;
    hence thesis by A10,FUNCT_1:1;
end;

reserve q,q1,q2,q3,q4 for FinSubsequence,
        p1,p2 for FinSequence;

theorem Th53:
  dom q1 misses dom q2 implies dom Shift(q1,i) misses dom Shift(q2,i)
proof
  assume
A1: dom q1 misses dom q2;
A2: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12;
A3: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12;
  now
    given x being object such that
A4: x in dom Shift(q1,i) /\ dom Shift(q2,i);
A5: x in dom Shift(q1,i) by A4,XBOOLE_0:def 4;
A6: x in dom Shift(q2,i) by A4,XBOOLE_0:def 4;
A7: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A2,A5;
    consider k2 being Nat such that
A8: x = k2+i and
A9: k2 in dom q2 by A3,A6;
    k2 in dom q1 /\ dom q2 by A7,A8,A9,XBOOLE_0:def 4;
    hence contradiction by A1;
  end;
  hence dom Shift(q1,i) /\ dom Shift(q2,i) = {} by XBOOLE_0:def 1;
end;

theorem
  for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
  Shift(q1,i) \/ Shift(q2,i) = Shift(q,i)
proof
  let q,q1,q2 be FinSubsequence such that
A1: q = q1 \/ q2 and
A2: q1 misses q2;
A3: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A4: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12;
A5: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12;
A6: q1 c= q by A1,XBOOLE_1:7;
A7: q2 c= q by A1,XBOOLE_1:7;
A8: Shift(q1,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7;
A9: Shift(q2,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7;
  dom q1 misses dom q2 by A2,A6,A7,FUNCT_1:112;
  then dom Shift(q1,i) misses dom Shift(q2,i) by Th53;
  then reconsider q3 = Shift(q1,i) \/ Shift(q2,i) as Function by GRFUNC_1:13;
  let x,y be object;
  thus [x,y] in Shift(q1,i) \/ Shift(q2,i) implies [x,y] in Shift(q,i)
  proof
    assume
A10: [x,y] in Shift(q1,i) \/ Shift(q2,i);
    then x in dom q3 by FUNCT_1:1;
    then
A11: x in dom Shift(q1,i) \/ dom Shift(q2,i) by XTUPLE_0:23;
A12: now
      assume
A13:  x in dom Shift(q1,i);
A14:  dom Shift(q1,i) c= dom Shift(q,i) by A8,GRFUNC_1:2;
      Shift(q1,i).x = Shift(q,i).x by A8,A13,GRFUNC_1:2;
      then [x,Shift(q,i).x] in Shift(q1,i) by A13,FUNCT_1:def 2;
      then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3;
      hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A13,A14,FUNCT_1:def 1
;
    end;
    now
      assume
A15:  x in dom Shift(q2,i);
A16:  dom Shift(q2,i) c= dom Shift(q,i) by A9,GRFUNC_1:2;
      Shift(q2,i).x = Shift(q,i).x by A9,A15,GRFUNC_1:2;
      then [x,Shift(q,i).x] in Shift(q2,i) by A15,FUNCT_1:def 2;
      then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3;
      hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A15,A16,FUNCT_1:def 1
;
    end;
    hence thesis by A11,A12,FUNCT_1:1,XBOOLE_0:def 3;
  end;
  assume
A17: [x,y] in Shift(q,i);
  then
A18: x in dom Shift(q,i) by FUNCT_1:1;
A19: y = Shift(q,i).x by A17,FUNCT_1:1;
  consider k being Nat such that
A20: x = k+i and
A21: k in dom q by A3,A18;
  dom q = dom q1 \/ dom q2 by A1,XTUPLE_0:23;
  then
A22: k in dom q1 or k in dom q2 by A21,XBOOLE_0:def 3;
  then x in dom Shift(q1,i) or x in dom Shift(q2,i) by A4,A5,A20;
  then x in dom Shift(q1,i) \/ dom Shift(q2,i) by XBOOLE_0:def 3;
  then
A23: x in dom q3 by XTUPLE_0:23;
A24: now
    assume
A25: x in dom Shift(q1,i);
    then
A26: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A4;
    thus y = q.k by A19,A20,A21,Def12
      .= q1.k by A1,A20,A26,GRFUNC_1:15
      .= Shift(q1,i).x by A20,A26,Def12
      .= q3.x by A25,GRFUNC_1:15;
  end;
  now
    assume
A27: x in dom Shift(q2,i);
    then
A28: ex k2 being Nat st ( x = k2+i)&( k2 in dom q2) by A5;
    thus y = q.k by A19,A20,A21,Def12
      .= q2.k by A1,A20,A28,GRFUNC_1:15
      .= Shift(q2,i).x by A20,A28,Def12
      .= q3.x by A27,GRFUNC_1:15;
  end;
  hence thesis by A4,A5,A20,A22,A23,A24,FUNCT_1:1;
end;

theorem Th55:
  for q being FinSubsequence holds dom Seq q = dom Seq Shift(q,i)
proof
  let q be FinSubsequence;
A1: len Seq q = card q by FINSEQ_3:158;
A2: len Seq Shift(q,i) = card Shift(q,i) by FINSEQ_3:158;
  thus dom Seq q = Seg len Seq q by FINSEQ_1:def 3
    .= dom Seq Shift(q,i) by Th41,A1,A2,FINSEQ_1:def 3;
end;

reserve l1 for Nat,
        j2 for Element of NAT;

theorem Th56:
  for q being FinSubsequence st k in dom Seq q
  ex j st j = (Sgm dom q).k & (Sgm dom Shift(q,i)).k = i + j
proof
  let q be FinSubsequence such that
A1: k in dom Seq q;
  consider ss being FinSubsequence such that
A2: dom ss = dom q and
A3: rng ss = dom Shift(q,i) and
A4: for l st l in dom q holds ss.l = i+l
  and ss is one-to-one by Th40;
A5: rng Seq ss = dom Shift(q,i) by A3,FINSEQ_1:101;
A6: rng Sgm dom q = dom q by FINSEQ_1:50;
A7: dom Seq q = dom (q*Sgm dom q)
    .= dom Sgm dom q by A6,RELAT_1:27;
A8: for l1 st l1 in dom Seq q
  ex j1 st j1 = (Sgm dom q).l1 & (Seq ss).l1 = i+j1
  proof
    let l1 such that
A9: l1 in dom Seq q;
A10: (Sgm dom q).l1 in rng Sgm dom q by A7,A9,FUNCT_1:def 3;
    then
A11: (Sgm dom q).l1 in dom q by FINSEQ_1:50;
    reconsider j1 = (Sgm dom q).l1 as Element of NAT by A10;
    (Seq ss).l1 = (ss*Sgm dom ss).l1
      .= ss.j1 by A2,A7,A9,FUNCT_1:13
      .= i+j1 by A4,A11;
    hence thesis;
  end;
A12: rng ss = rng Sgm dom Shift(q,i) by A3,FINSEQ_1:50;
  rng Sgm dom Shift(q,i) c= NAT;
  then rng Seq ss c= NAT by A12,FINSEQ_1:101;
  then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def 4;
A13: ex l2 be Nat st ( dom Shift(q,i) c= Seg l2) by FINSEQ_1:def 12;
A14: dom Seq ss = dom (ss*Sgm dom ss)
    .= dom Sgm dom q by A2,A6,RELAT_1:27;
  for n,m,k1,k2 being Nat st 1 <= n & n < m & m <= len fs &
  k1 = fs.n & k2 = fs.m holds k1 < k2
  proof
    let n,m,k1,k2 be Nat;
    assume that
A15: 1 <= n and
A16: n < m and
A17: m <= len fs and
A18: k1 = fs.n and
A19: k2 = fs.m;
    reconsider n,m as Element of NAT by ORDINAL1:def 12;
A20: dom fs = Seg len fs by FINSEQ_1:def 3
      .= {l3 where l3 is Nat: 1 <= l3 & l3 <= len fs};
    n+1 <= m by A16,INT_1:7;
    then n+1 <= len fs by A17,XXREAL_0:2;
    then
A21: n <= (len fs) - 1 by XREAL_1:19;
    (len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7;
    then (len fs) - 1 <= len fs by XREAL_1:20;
    then n <= len fs by A21,XXREAL_0:2;
    then
A22: n in dom Seq q by A7,A14,A15,A20;
    1 <= m by A15,A16,XXREAL_0:2;
    then
A23: m in dom Seq q by A7,A14,A17,A20;
    consider j2 being Element of NAT such that
A24: j2 = (Sgm dom q).n and
A25: fs.n = i+j2 by A8,A22;
    consider j3 being Element of NAT such that
A26: j3 = (Sgm dom q).m and
A27: fs.m = i+j3 by A8,A23;
A28: ex l3 being Nat st ( dom q c= Seg l3) by FINSEQ_1:def 12;
    dom Seq ss = Seg len fs by FINSEQ_1:def 3;
    then len fs = len Sgm dom q by A14,FINSEQ_1:def 3;
    then j2 < j3 by A15,A16,A17,A24,A26,A28,FINSEQ_1:def 13;
    hence thesis by A18,A19,A25,A27,XREAL_1:8;
  end;
  then fs = Sgm dom Shift(q,i) by A5,A13,FINSEQ_1:def 13;
  hence thesis by A1,A8;
end;

theorem Th57:
  for q being FinSubsequence st
  k in dom Seq q holds (Seq Shift(q,i)).k = (Seq q).k
proof
  let q be FinSubsequence;
  assume
A1: k in dom Seq q;
  then consider j such that
A2: j = (Sgm dom q).k and
A3: (Sgm dom Shift(q,i)).k = i+j by Th56;
A4: rng Sgm dom q = dom q by FINSEQ_1:50;
A5: dom Seq q = dom Seq Shift(q,i) by Th55
    .= dom (Shift(q,i)*(Sgm dom Shift(q,i)));
A6: dom Seq q = dom (q*Sgm dom q)
    .= dom Sgm dom q by A4,RELAT_1:27;
  then j in rng Sgm dom q by A1,A2,FUNCT_1:def 3;
  then
A7: j in dom q by FINSEQ_1:50;
  (Seq Shift(q,i)).k = (Shift(q,i)*(Sgm dom Shift(q,i))).k
    .= Shift(q,i).((Sgm dom Shift(q,i)).k)
  by A1,A5,FUNCT_1:12
    .= q.j by A3,A7,Def12
    .= (q*Sgm dom q).k by A1,A2,A6,FUNCT_1:13
    .= (Seq q).k;
  hence thesis;
end;

theorem
  for q being FinSubsequence holds Seq q = Seq Shift(q,i)
proof
  let q be FinSubsequence;
A1: dom Seq q = dom Seq Shift(q,i) by Th55;
  for x being object holds
   x in dom Seq q implies (Seq Shift(q,i)).x = (Seq q).x by Th57;
  hence thesis by A1;
end;

theorem Th59:
  for q being FinSubsequence st
  dom q c= Seg k holds dom Shift(q,i) c= Seg (i+k)
proof
  let q be FinSubsequence;
  assume
A1: dom q c= Seg k;
A2: dom Shift(q,i) = {j+i where j is Nat: j in dom q} by Def12;
  let x be object;
  assume x in dom Shift(q,i);
  then consider j1 being Nat such that
A3: x = j1+i and
A4: j1 in dom q by A2;
  j1 in Seg k by A1,A4;
  then
A5: ex j2 being Nat st ( j1 = j2)&( 1 <= j2)&( j2 <= k);
A6: 0 qua Nat+1 <= i+j1 by A5,XREAL_1:7;
  i+j1 <= i+k by A5,XREAL_1:7;
  hence thesis by A3,A6;
end;

theorem Th60:
  for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p
  ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p)
proof
  let p be FinSequence, q1,q2 be FinSubsequence;
  assume q1 c= p;
  then
A1: dom q1 c= dom p by GRFUNC_1:2;
  dom p misses dom Shift(q2,len p) by Th47;
  then reconsider ss = q1 \/ Shift(q2,len p) as Function by A1,GRFUNC_1:13
,XBOOLE_1:63;
A2: dom p = Seg len p by FINSEQ_1:def 3;
  consider k be Nat such that
A3: dom q2 c= Seg k by FINSEQ_1:def 12;
  k in NAT by ORDINAL1:def 12;
  then
A4: dom Shift(q2,len p) c= Seg (len p + k) by A3,Th59;
  len p + (0 qua Nat) <= len p + k by XREAL_1:7;
  then Seg len p c= Seg (len p + k) by FINSEQ_1:5;
  then dom q1 c= Seg (len p + k) by A1,A2;
  then dom q1 \/ dom Shift(q2,len p) c= Seg (len p + k) by A4,XBOOLE_1:8;
  then dom (q1 \/ Shift(q2,len p)) c= Seg (len p + k) by XTUPLE_0:23;
  then reconsider ss as FinSubsequence by FINSEQ_1:def 12;
  take ss;
  thus thesis;
end;

Lm7: for p,q being FinSubsequence st q c= p holds
dom Shift(q,i) c= dom Shift(p,i)
proof
  let p,q be FinSubsequence;
  assume
A1: q c= p;
A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12;
A4: dom q c= dom p by A1,GRFUNC_1:2;
  let x be object;
  assume x in dom Shift(q,i);
  then ex k1 being Nat st ( x = k1+i)&( k1 in dom q) by A2;
  hence thesis by A3,A4;
end;

Lm8: for p1,p2 being FinSequence, q1,q2 being FinSubsequence st
q1 c= p1 & q2 c= p2 holds Sgm (dom q1 \/ dom Shift(q2,len p1))
= (Sgm dom q1)^(Sgm dom Shift(q2,len p1))
proof
  let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
  assume that
A1: q1 c= p1 and
A2: q2 c= p2;
A3: ex k1 be Nat st ( dom q1 c= Seg k1) by FINSEQ_1:def 12;
A4: ex k2 be Nat st ( dom Shift(q2,len p1) c= Seg k2) by FINSEQ_1:def 12;
  for m,n being Nat
  st m in dom q1 & n in dom Shift(q2,len p1) holds m < n
  proof
    let m,n be Nat such that
A5: m in dom q1 and
A6: n in dom Shift(q2,len p1);
A7: dom p1 = Seg len p1 by FINSEQ_1:def 3
      .= {k where k is Nat: 1 <= k & k <= len p1};
A8: dom Shift(p2,len p1)
   = {k where k is Nat : len p1 + 1 <= k & k <= len p1 + len p2}
    by Th39;
A9: dom q1 c= dom p1 by A1,GRFUNC_1:2;
A10: dom Shift(q2,len p1) c= dom Shift(p2,len p1) by A2,Lm7;
A11: m in dom p1 by A5,A9;
A12: n in dom Shift(p2,len p1) by A6,A10;
    consider k3 being Nat such that
A13: k3 = m
    and 1 <= k3 and
A14: k3 <= len p1 by A7,A11;
    consider k4 being Nat such that
A15: k4 = n and
A16: len p1 + 1 <= k4
    and k4 <= len p1 + len p2 by A8,A12;
    len p1 < len p1 + 1 by XREAL_1:29;
    then k3 <= len p1 + 1 by A14,XXREAL_0:2;
    then
A17: k3 <= k4 by A16,XXREAL_0:2;
    k3 <> k4 by A5,A6,A9,A13,A15,Th47,XBOOLE_0:3;
    hence thesis by A13,A15,A17,XXREAL_0:1;
  end;
  hence thesis by A3,A4,FINSEQ_3:42;
end;

theorem Th61:
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
  ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) &
  dom Seq ss = Seg (len Seq q1 + len Seq q2)
proof
  let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
  assume that
A1: q1 c= p1 and
A2: q2 c= p2;
    consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) by A1,Th60;
A4: ex k1 be Nat st ( dom q1 c= Seg k1) by FINSEQ_1:def 12;
A5: ex k2 be Nat st ( dom Shift(q2,len p1) c= Seg k2) by FINSEQ_1:def 12;
A6: rng Sgm dom ss = dom ss by FINSEQ_1:50;
A7: dom Seq ss = dom Sgm dom ss by A6,RELAT_1:27
      .= dom Sgm (dom q1 \/ dom Shift(q2,len p1)) by A3,XTUPLE_0:23
      .= dom ((Sgm dom q1)^(Sgm dom Shift(q2,len p1))) by A1,A2,Lm8
      .= Seg (len Sgm dom q1 + len Sgm dom Shift(q2,len p1))
    by FINSEQ_1:def 7;
A8: len Sgm dom Shift(q2,len p1) = card dom Shift(q2,len p1) by A5,FINSEQ_3:39;
A9: len Sgm dom q1 = card dom q1 by A4,FINSEQ_3:39;
    len Sgm dom Shift(q2,len p1) = card Shift(q2,len p1) by A8,CARD_1:62;
    then
A10: len Sgm dom Shift(q2,len p1) = card q2 by Th41;
A11: len Sgm dom q1 = card q1 by A9,CARD_1:62;
A12: len Sgm dom Shift(q2,len p1) = len Seq q2 by A10,FINSEQ_3:158;
    len Sgm dom q1 = len Seq q1 by A11,FINSEQ_3:158;
    hence thesis by A3,A7,A12;
end;

theorem Th62:
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
  ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) &
  dom Seq ss = Seg (len Seq q1 + len Seq q2) &
  Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1)
proof
  let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
  assume that
A1: q1 c= p1 and
A2: q2 c= p2;
  consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) and
A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) by A1,A2,Th61;
A5: dom Seq q1 = Seg len Seq q1 by FINSEQ_1:def 3
      .= {k where k is Nat: 1 <= k & k <= len Seq q1};
A6: dom Shift(Seq q2,len Seq q1)
    = {k where k is Nat: len Seq q1 + 1 <= k & k <= len Seq q1 + len Seq q2}
          by Th39;
A7: Seg (len Seq q1 + len Seq q2)
    = dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
    proof
      thus Seg (len Seq q1 + len Seq q2)
      c= dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
      proof
        let x be object;
        assume x in Seg (len Seq q1 + len Seq q2);
        then consider k1 being Nat such that
A8:    x = k1 and
A9:    1 <= k1 and
A10:    k1 <= len Seq q1 + len Seq q2;
A11:    1 <= k1 & k1 <= len Seq q1 implies k1 in dom Seq q1 by A5;
        len Seq q1 + 1 <= k1 & k1 <= len Seq q1 + len Seq q2 implies
        k1 in dom Shift(Seq q2,len Seq q1) by A6;
        hence thesis by A8,A9,A10,A11,INT_1:7,XBOOLE_0:def 3;
      end;
      let x be object;
      assume
A12:  x in dom Seq q1 \/ dom Shift(Seq q2,len Seq q1);
A13:  now
        assume x in dom Seq q1;
        then consider k1 being Nat such that
A14:    x = k1 and
A15:    1 <= k1 and
A16:    k1 <= len Seq q1 by A5;
        len Seq q1 + (0 qua Nat) <= len Seq q1 + len Seq q2 by XREAL_1:7;
        then k1 <= len Seq q1 + len Seq q2 by A16,XXREAL_0:2;
        hence thesis by A14,A15;
      end;
      now
        assume x in dom Shift(Seq q2,len Seq q1);
        then consider k2 being Nat such that
A17:    x = k2 and
A18:    len Seq q1 + 1 <= k2 and
A19:    k2 <= len Seq q1 + len Seq q2 by A6;
        0 qua Nat+1 <= len Seq q1 + 1 by XREAL_1:7;
        then 1 <= k2 by A18,XXREAL_0:2;
        hence thesis by A17,A19;
      end;
      hence thesis by A12,A13,XBOOLE_0:def 3;
    end;
A20: dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
    = dom (Seq q1 \/ Shift(Seq q2,len Seq q1)) by XTUPLE_0:23;
    dom Seq q1 misses dom Shift(Seq q2,len Seq q1) by Th47;
    then reconsider ss1 = Seq q1 \/ Shift(Seq q2,len Seq q1) as Function
    by GRFUNC_1:13;
    for x being object st x in dom Seq ss holds (Seq ss).x = ss1.x
    proof
      let x be object;
      assume
A21:  x in dom Seq ss;
A22:  (Seq ss).x = (ss*Sgm dom ss).x
        .= ss.((Sgm dom ss).x) by A21,FUNCT_1:12
        .= ss.((Sgm (dom q1 \/ dom Shift(q2,len p1))).x) by A3,XTUPLE_0:23
        .= ss.(((Sgm dom q1)^(Sgm dom Shift(q2,len p1))).x) by A1,A2,Lm8;
A23:  now
        assume
A24:    x in dom Seq q1;
        then
A25:    x in dom Sgm dom q1 by FINSEQ_1:100;
        then (Sgm dom q1).x in rng Sgm dom q1 by FUNCT_1:def 3;
        then
A26:    (Sgm dom q1).x in dom q1 by FINSEQ_1:50;
        (Seq ss).x = ss.((Sgm dom q1).x) by A22,A25,FINSEQ_1:def 7
          .= q1.((Sgm dom q1).x) by A3,A26,GRFUNC_1:15
          .= (q1*Sgm dom q1).x by A25,FUNCT_1:13
          .= (Seq q1).x;
        hence thesis by A24,GRFUNC_1:15;
      end;
      now
        assume
A27:    x in dom Shift(Seq q2,len Seq q1);
        dom Shift(Seq q2,len Seq q1)
          = {j+len Seq q1 where j is Nat: j in dom Seq q2 }
        by Def12;
        then consider j being Nat such that
A28:    x = j+len Seq q1 and
A29:    j in dom Seq q2 by A27;
A30:    ss1.x = Shift(Seq q2,len Seq q1).x by A27,GRFUNC_1:15
          .= (Seq q2).j by A28,A29,Def12;
A31:    ex l1 be Nat st ( dom q1 c= Seg l1) by FINSEQ_1:def 12;
A32:    ex l2 be Nat st ( dom Shift(q2,len p1) c= Seg l2) by FINSEQ_1:def 12;
        card dom q1 = len Sgm dom q1 by A31,FINSEQ_3:39;
        then
A33:    card q1 = len Sgm dom q1 by CARD_1:62;
A34:    len Seq q1 = card q1 by FINSEQ_3:158;
A35:    dom Seq q2 = Seg len Seq q2 by FINSEQ_1:def 3;
        card q2 = len Seq q2 by FINSEQ_3:158;
        then
A36:    card Shift(q2,len p1) = len Seq q2 by Th41;
        then
A37:    card dom Shift(q2,len p1) = len Seq q2 by CARD_1:62;
A38:    card dom Shift(q2,len p1) = len Sgm dom Shift(q2,len p1)
        by A32,FINSEQ_3:39;
A39:    len Sgm dom Shift(q2,len p1) = len Seq q2 by A32,A37,FINSEQ_3:39;
A40:    dom Seq q2 = dom Sgm dom Shift(q2,len p1) by A35,A36,A38,CARD_1:62
,FINSEQ_1:def 3;
A41:    j in dom Sgm dom Shift(q2,len p1) by A29,A35,A39,FINSEQ_1:def 3;
        (Sgm dom Shift(q2,len p1)).j in rng Sgm dom Shift(q2,len p1)
        by A29,A40,FUNCT_1:def 3;
        then
A42:    (Sgm dom Shift(q2,len p1)).j in dom Shift(q2,len p1) by FINSEQ_1:50;
        (Seq ss).x
        = ss.((Sgm dom Shift(q2,len p1)).j) by A22,A28,A33,A34,A41,
FINSEQ_1:def 7
          .= Shift(q2,len p1).((Sgm dom Shift(q2,len p1)).j)
        by A3,A42,GRFUNC_1:15
          .= (Shift(q2,len p1)*(Sgm dom Shift(q2,len p1))).j
        by A29,A40,FUNCT_1:13
          .= (Seq Shift(q2,len p1)).j
          .= (Seq q2).j by A29,Th57;
        hence thesis by A30;
      end;
      hence thesis by A4,A7,A21,A23,XBOOLE_0:def 3;
    end;
    then Seq ss = ss1 by A4,A7,A20;
    hence thesis by A3,A4;
end;

theorem
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
  ex ss being FinSubsequence st
  ss = q1 \/ Shift(q2,len p1) & (Seq q1)^(Seq q2) = Seq ss
proof
  let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
  assume that
A1: q1 c= p1 and
A2: q2 c= p2;
  consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) and
A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) and
A5: Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1) by A1,A2,Th62;
A6: for j1 be Nat st j1 in dom Seq q1 holds (Seq ss).j1 = (Seq q1).j1
  by A5,GRFUNC_1:15;
  for j2 be Nat st j2 in dom Seq q2 holds (Seq ss).(len Seq q1 + j2) =
  (Seq q2).j2
  proof
    let j2 be Nat;
    assume
A7: j2 in dom Seq q2;
    dom Shift(Seq q2,len Seq q1) =
      {k+len Seq q1 where k is Nat: k in dom Seq q2} by Def12;
    then len Seq q1 + j2 in dom Shift(Seq q2,len Seq q1) by A7;
    hence (Seq ss).(len Seq q1 + j2)
    = Shift(Seq q2,len Seq q1).(len Seq q1 + j2) by A5,GRFUNC_1:15
      .= (Seq q2).j2 by A7,Def12;
  end;
  then Seq ss = (Seq q1)^(Seq q2) by A4,A6,FINSEQ_1:def 7;
  hence thesis by A3;
end;

theorem
  for F being non empty NAT-defined finite Function
  holds card CutLastLoc F = card F -' 1
proof let F be non empty NAT-defined finite Function;
A1: card F >= 0+1 by NAT_1:13;
 thus card CutLastLoc F = card F - 1 by Th37
            .= card F -' 1 by A1,XREAL_1:233;
end;

theorem
  for F,G being non empty NAT-defined finite Function
    st dom F = dom G
  holds LastLoc F = LastLoc G;

theorem
 for f being non empty NAT-defined finite Function
 holds Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y)
 proof let f be non empty NAT-defined finite Function;
A1: dom f = dom(f +~ (x,y)) by FUNCT_4:99;
A2: dom(Shift(f,i) +~ (x,y))
    = dom Shift(f,i) by FUNCT_4:99
   .= { m+i where m is Nat:m in dom(f +~ (x,y)) } by A1,Def12;
  for m being Nat st m in dom(f +~ (x,y))
    holds (Shift(f,i) +~ (x,y)).(m+i) = (f +~ (x,y)).m
  proof let m be Nat;
   assume m in dom(f +~ (x,y));
    then
A3:  m+i in dom(Shift(f,i) +~ (x,y)) by A2;
    then
A4:  m+i in dom Shift(f,i) by FUNCT_4:99;
    consider mm being Nat such that
A5:  m+i = mm+i and
A6:  mm in dom(f +~ (x,y)) by A2,A3;
    m = mm by A5;
    then m in dom(f +~ (x,y)) by A6;
    then
A7:  m in dom f by FUNCT_4:99;
    then
A8:  Shift(f,i).(m+i) = f.m by Def12;
   per cases;
   suppose
A9:   Shift(f,i).(m+i) = x;
   hence (Shift(f,i) +~ (x,y)).(m+i) = y by A4,FUNCT_4:106
    .= (f +~ (x,y)).m by A7,FUNCT_4:106,A9,A8;
   end;
   suppose
A10:  Shift(f,i).(m+i) <> x;
   hence (Shift(f,i) +~ (x,y)).(m+i)
      = Shift(f,i).(m+i) by FUNCT_4:105
     .= (f +~ (x,y)).m by A10,A8,FUNCT_4:105;
   end;
  end;

  hence Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y) by A2,Def12;
 end;

theorem
  for F, G being non empty NAT-defined finite Function st dom F c= dom G
   holds LastLoc F <= LastLoc G by XXREAL_2:59;