:: About Quotient Orders and Ordering Sequences
::  by Sebastian Koch
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 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, SUBSET_1, REAL_1, PARTFUN1, RELAT_1, ARYTM_1, FUNCT_1,
      ARYTM_3, TARSKI, XBOOLE_0, CARD_1, NAT_1, FUNCOP_1, XXREAL_0, CARD_3,
      FUNCT_2, RELAT_2, EQREL_1, STRUCT_0, ORDERS_2, REARRAN1, WELLFND1,
      FINSEQ_5, WAYBEL20, REALALG1, FINSEQ_2, PARTFUN3, ORDINAL4, CLASSES1,
      PRE_POLY, FINSET_1, DICKSON, FINSEQ_1, ORDERS_1, PETERSON, XCMPLX_0,
      ZFMISC_1, UPROOTS, ORDERS_5, PARTIT1;
 notations ORDINAL1, XCMPLX_0, XREAL_0, XXREAL_0, TARSKI, XBOOLE_0, SUBSET_1,
      NUMBERS, FUNCOP_1, RELAT_1, RELAT_2, CARD_1, CLASSES1, RELSET_1,
      VALUED_0, VALUED_1, FUNCT_1, PARTFUN1, FUNCT_2, PARTFUN3, FINSET_1,
      FINSEQ_2, FINSEQOP, RVSUM_1, FINSEQ_1, DICKSON, ORDERS_1, FINSEQ_3,
      FINSEQ_5, EQREL_1, STRUCT_0, NECKLACE, PRE_POLY, ORDERS_2, PARTIT1;
 constructors NAT_D, FINSEQ_5, PARTFUN3, RELSET_1, RVSUM_1, CLASSES1, PRE_POLY,
      MATRPROB, FINSEQOP, NECKLACE, DICKSON, PARTIT1;
 registrations XBOOLE_0, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, RELAT_1,
      RELAT_2, RELSET_1, EQREL_1, JORDAN23, VALUED_0, VALUED_1, FUNCT_1,
      FUNCT_2, PARTFUN3, STRUCT_0, ORDERS_2, NAT_1, FINSET_1, FINSEQ_1,
      PARTFUN1, RVSUM_1, PRE_POLY, CARD_1, SUBSET_1, FINSEQ_5;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

:: into SUBSET_1 ?
theorem :: ORDERS_5:1
  for A, B being set, x being object holds
    A = B \ {x} & x in B implies B \ A = {x};

:: into RELAT_1 ? present in FOMODEL0
registration
  let Y be set, X be Subset of Y;
  cluster X-defined -> Y-defined for Relation;
::  cluster X-valued -> Y-valued for Relation;
::  coherence by RELAT_1:183;
end;

:: placement in CARD_2 also seems appropriate because of CARD_2:60
theorem :: ORDERS_5:2
  for X being set, x being object st x in X & card X = 1 holds {x} = X;

:: into FINSEQ_1 ?
:: interesting enough, trivdemo didn't recognized this one as trivial
theorem :: ORDERS_5:3
  for X being set, k being Nat st X c= Seg k holds rng Sgm X c= Seg k;

:: into FINSEQ_1 ?
registration
  let s be FinSequence;
  let N be Subset of dom s;
  cluster s * Sgm(N) -> FinSequence-like;
end;

:: into FINSEQ_2 ?
:: compare FINSEQ_2:32
registration
  let A be set, B be Subset of A, C be non empty set,
  f be FinSequence of B, g be Function of A, C;
  cluster g*f -> FinSequence-like;
end;

:: into FINSEQ_2 ?
registration
  let s be FinSequence;
  cluster s * idseq len(s) -> FinSequence-like;
end;

:: into FINSEQ_5 ?
registration
  let s be FinSequence;
  reduce Rev Rev(s) to s;
end;

:: into FINSET_1 ?
scheme :: ORDERS_5:sch 1
 Finite2{A()->set, B()->Subset of A(), P[set]} : P[A()]
provided
 A() is finite and
 P[B()] and
 for x,C being set st x in A()\B() & B() c= C & C c= A() & P[C] holds
      P[C \/ {x}];

:: into STRUCT_0 ?
:: actually, I'm not sure why this redefinition is even needed by the analyzer
definition
  let S, T be 1-sorted, f be Function of S, T;
  let B be Subset of S;
  redefine func f.:B -> Subset of T;
end;

::$CT

:: into RVSUM_1 ?
theorem :: ORDERS_5:5
  for s being FinSequence of REAL st Sum s <> 0 holds
    ex i being Nat st i in dom s & s.i <> 0;

:: into RVSUM_1 ?
:: similar to RVSUM_1:85
theorem :: ORDERS_5:6
  for s being FinSequence of REAL st s is nonnegative-yielding &
    ex i being Nat st i in dom s & s.i <> 0 holds
      Sum s > 0;

:: into RVSUM_1 ?
:: used the preceeding proof to proof this one, which seemed to be both:
:: a good exercise and a demonstration of symmetry
:: However, a copy and paste proof would need less article references
theorem :: ORDERS_5:7
  for s being FinSequence of REAL st s is nonpositive-yielding &
    ex i being Nat st i in dom s & s.i <> 0 holds
      Sum s < 0;

:: into RFINSEQ ?
theorem :: ORDERS_5:8
  for X being set, s,t being FinSequence of X, f being Function of X, REAL st
    s is one-to-one & t is one-to-one & rng t c= rng s &
    for x being Element of X st x in rng s \ rng t holds f.x = 0 holds
      Sum (f * s) = Sum (f * t);

:: into PARTFUN3 ?
registration
  let X be set;
  let f be Function, g be positive-yielding Function of X,REAL;
  cluster g*f -> positive-yielding;
end;

:: into PARTFUN3 ?
registration
  let X be set;
  let f be Function, g be negative-yielding Function of X,REAL;
  cluster g*f -> negative-yielding;
end;

:: into PARTFUN3 ?
registration
  let X be set;
  let f be Function, g be nonpositive-yielding Function of X,REAL;
  cluster g*f -> nonpositive-yielding;
end;

:: into PARTFUN3 ?
registration
  let X be set;
  let f be Function, g be nonnegative-yielding Function of X,REAL;
  cluster g*f -> nonnegative-yielding;
end;

:: into PRE_POLY ?
definition
  let s be Function;
  redefine func support s -> Subset of dom s;
end;

::: into PRE_POLY ?
registration
  let X be set;
  cluster finite-support nonnegative-yielding for Function of X, REAL;
end;

::: into PRE_POLY ?
registration
  let X be set;
  cluster nonnegative-yielding finite-support for Function of X, COMPLEX;
end;

:: into CFUNCT_1 ?
theorem :: ORDERS_5:9
  for A being set, f being Function of A, COMPLEX holds
    support f = support -f;

:: into CFUNCT_1 ?
registration
  let A be set, f be finite-support Function of A, COMPLEX;
  cluster -f -> finite-support;
end;

:: into CFUNCT_1 as a consequence?
registration
  let A be set, f be finite-support Function of A, REAL;
  cluster -f -> finite-support;
end;

begin :: Orders

theorem :: ORDERS_5:10
  for X being set, R being Relation, Y being Subset of X st
    R is_irreflexive_in X holds R is_irreflexive_in Y;

theorem :: ORDERS_5:11
  for X being set, R being Relation, Y being Subset of X st
    R is_symmetric_in X holds R is_symmetric_in Y;

theorem :: ORDERS_5:12
  for X being set, R being Relation, Y being Subset of X st
    R is_asymmetric_in X holds R is_asymmetric_in Y;

definition
  let A be RelStr;
  attr A is connected means
:: ORDERS_5:def 1
  the InternalRel of A is_connected_in the carrier of A;
  attr A is strongly_connected means
:: ORDERS_5:def 2
  the InternalRel of A is_strongly_connected_in the carrier of A;
end;

registration
  cluster non empty reflexive transitive antisymmetric connected
    strongly_connected strict total for RelStr;
end;

registration
  cluster strongly_connected -> reflexive connected for RelStr;
end;

registration
  cluster reflexive connected -> strongly_connected for RelStr;
end;

registration
  cluster empty -> reflexive antisymmetric transitive connected
    strongly_connected for RelStr;
end;

definition
  let A be RelStr;
  let a1, a2 be Element of A;
  pred a1 =~ a2 means
:: ORDERS_5:def 3

  a1 <= a2 & a2 <= a1;
end;

theorem :: ORDERS_5:13
  for A being reflexive non empty RelStr, a being Element of A holds a =~ a;

definition
  let A be reflexive non empty RelStr;
  let a1, a2 be Element of A;
  redefine pred a1 =~ a2;
  reflexivity;
end;

definition
  let A be RelStr;
  let a1, a2 be Element of A;
  pred a1 <~ a2 means
:: ORDERS_5:def 4
  a1 <= a2 & not a2 <= a1;
  irreflexivity;
end;

notation
  let A be RelStr;
  let a1, a2 be Element of A;
  synonym a2 >~ a1 for a1 <~ a2;
end;

definition
  let A be connected RelStr;
  let a1, a2 be Element of A;
  redefine pred a1 <~ a2;
  asymmetry;
end;

theorem :: ORDERS_5:14
  for A being non empty RelStr,
    a1, a2 being Element of A st A is strongly_connected holds
      a1 <~ a2 or a1 =~ a2 or a1 >~ a2;

theorem :: ORDERS_5:15
  for A being transitive RelStr, a1,a2,a3 being Element of A holds
    (a1 <~ a2 & a2 <= a3 implies a1 <~ a3) &
    (a1 <= a2 & a2 <~ a3 implies a1 <~ a3);

theorem :: ORDERS_5:16
  for A being non empty RelStr, a1,a2 being Element of A st
    A is strongly_connected holds
      a1 <= a2 or a2 <= a1;

theorem :: ORDERS_5:17
  for A being non empty RelStr, B being Subset of A,
    a1,a2 being Element of A st
      the InternalRel of A is_connected_in B & a1 in B & a2 in B & a1 <> a2
      holds
        a1 <= a2 or a2 <= a1;

theorem :: ORDERS_5:18
  for A being non empty RelStr, a1,a2 being Element of A st
    A is connected & a1 <> a2 holds
      a1 <= a2 or a2 <= a1;

theorem :: ORDERS_5:19
  for A being non empty RelStr, a1,a2 being Element of A st
    A is strongly_connected holds
      a1 = a2 or a1 < a2 or a2 < a1;

theorem :: ORDERS_5:20
  for A being RelStr, a1, a2 being Element of A
    st a1 <= a2 holds a1 in the carrier of A & a2 in the carrier of A;

theorem :: ORDERS_5:21
  for A being RelStr, a1, a2 being Element of A
    st a1 <= a2 holds A is non empty;

theorem :: ORDERS_5:22
  for A being transitive RelStr, B being finite Subset of A
    st B is non empty & the InternalRel of A is_connected_in B holds
      ex x being Element of A st x in B &
        for y being Element of A st y in B & x <> y holds
          x <= y;

theorem :: ORDERS_5:23
  for A being connected transitive RelStr, B being finite Subset of A
    st B is non empty holds
      ex x being Element of A st x in B &
        for y being Element of A st y in B & x <> y holds
          x <= y;

theorem :: ORDERS_5:24
  for A being transitive RelStr, B being finite Subset of A
    st B is non empty & the InternalRel of A is_connected_in B holds
      ex x being Element of A st x in B &
        for y being Element of A st y in B & x <> y holds
          y <= x;

theorem :: ORDERS_5:25
  for A being connected transitive RelStr, B being finite Subset of A
    st B is non empty holds
      ex x being Element of A st x in B &
        for y being Element of A st y in B & x <> y holds
          y <= x;

:: I repeated some definitions here to have them all in one place

definition
  mode Preorder is reflexive transitive RelStr;
  mode LinearPreorder is strongly_connected transitive RelStr;
  mode Order is reflexive antisymmetric transitive RelStr;
  mode LinearOrder is strongly_connected antisymmetric transitive RelStr;
end;

registration
  cluster -> quasi_ordered for Preorder;
end;

registration
  cluster empty for LinearOrder;
end;

theorem :: ORDERS_5:26
  for A being Preorder holds
    the InternalRel of A quasi_orders the carrier of A;

theorem :: ORDERS_5:27
  for A being Order holds
    the InternalRel of A partially_orders the carrier of A;

theorem :: ORDERS_5:28
  for A being LinearOrder holds
    the InternalRel of A linearly_orders the carrier of A;

theorem :: ORDERS_5:29
  for A being RelStr st the InternalRel of A quasi_orders the carrier of A
  holds A is reflexive transitive;

theorem :: ORDERS_5:30
  for A being RelStr st the InternalRel of A partially_orders the carrier of A
  holds A is reflexive transitive antisymmetric;

theorem :: ORDERS_5:31
  for A being RelStr st the InternalRel of A linearly_orders the carrier of A
  holds A is reflexive transitive antisymmetric connected;

scheme :: ORDERS_5:sch 2
  RelStrMin{A()->transitive connected RelStr, B()->finite Subset of A(),
    P[Element of A()]} :
    ex x being Element of A() st x in B() & P[x] &
      for y being Element of A() st y in B() & y <~ x holds not P[y]
provided
   ex x being Element of A() st x in B() & P[x];

scheme :: ORDERS_5:sch 3
  RelStrMax{A()->transitive connected RelStr, B()->finite Subset of A(),
    P[Element of A()]} :
    ex x being Element of A() st x in B() & P[x] &
      for y being Element of A() st y in B() & x <~ y holds not P[y]
provided
   ex x being Element of A() st x in B() & P[x];

begin :: Quotient Order

definition
::$CD
  let A be Preorder;
  func EqRelOf A -> Equivalence_Relation of the carrier of A means
:: ORDERS_5:def 6

  for x, y being Element of A holds [x,y] in it iff x <= y & y <= x;
end;

theorem :: ORDERS_5:32
  for A being Preorder holds EqRelOf A = EqRel A;

registration
  let A be empty Preorder;
  cluster EqRelOf A -> empty;
end;

registration
  let A be non empty Preorder;
  cluster EqRelOf A -> non empty;
end;

theorem :: ORDERS_5:33
  for A being Order holds
    EqRelOf A = id the carrier of A;

definition
  let A be Preorder;
  func QuotientOrder(A) -> strict RelStr means
:: ORDERS_5:def 7

    the carrier of it = Class EqRelOf A &
    for X, Y being Element of Class EqRelOf A holds
       [X, Y] in the InternalRel of it iff
         ex x, y being Element of A st
           X = Class(EqRelOf A, x) & Y = Class(EqRelOf A, y) & x <= y;
end;

registration
  let A be empty Preorder;
  cluster QuotientOrder(A) -> empty;
end;

theorem :: ORDERS_5:34
  for A being non empty Preorder, x being Element of A holds
    Class(EqRelOf A, x) in the carrier of QuotientOrder(A);

registration
  let A be non empty Preorder;
  cluster QuotientOrder(A) -> non empty;
end;

theorem :: ORDERS_5:35
  for A being Preorder holds the InternalRel of QuotientOrder(A) = <=E A;

registration
  let A be Preorder;
  cluster QuotientOrder(A) -> reflexive total antisymmetric transitive;
end;

:: this generalizes DICKSON:10 to possibly empty RelStr
registration
  let A be LinearPreorder;
  cluster QuotientOrder(A) -> connected strongly_connected;
end;

definition
  let A be Preorder;
  func proj A -> Function of A, QuotientOrder(A) means
:: ORDERS_5:def 8

  for x being Element of A holds it.x = Class(EqRelOf A, x);
end;

registration
  let A be empty Preorder;
  cluster proj A -> empty;
end;

registration
  let A be non empty Preorder;
  cluster proj A -> non empty;
end;

theorem :: ORDERS_5:36
  for A being non empty Preorder, x, y being Element of A st x <= y holds
   (proj A).x <= (proj A).y;

theorem :: ORDERS_5:37
  for A being Preorder,
    x,y being Element of A holds
      x =~ y implies (proj A).x = (proj A).y;

definition
  let A be Preorder, R be Equivalence_Relation of the carrier of A;
  attr R is EqRelOf-like means
:: ORDERS_5:def 9
  R = EqRelOf A;
end;

registration
  let A be Preorder;
  cluster EqRelOf A -> EqRelOf-like;
end;

registration
  let A be Preorder;
  cluster EqRelOf-like for Equivalence_Relation of the carrier of A;
end;

definition
  let A be Preorder,
    R be EqRelOf-like Equivalence_Relation of the carrier of A;
  let x be Element of A;
  redefine func Class(R, x) -> Element of QuotientOrder(A);
end;

theorem :: ORDERS_5:38
  for A being Preorder holds
    the carrier of QuotientOrder(A) is a_partition of the carrier of A;

theorem :: ORDERS_5:39
  for A being non empty Preorder,
    D being non empty a_partition of the carrier of A
  st D = the carrier of QuotientOrder(A) holds
    proj A = proj D;

definition
  let A be set, D be a_partition of A;
  func PreorderFromPartition(D) -> strict RelStr equals
:: ORDERS_5:def 10
  RelStr(#A, ERl D#);
end;

registration
  let A be non empty set, D be a_partition of A;
  cluster PreorderFromPartition(D) -> non empty;
end;

registration
  let A be set, D be a_partition of A;
  cluster PreorderFromPartition(D) -> reflexive transitive;
  cluster PreorderFromPartition(D) -> symmetric;
end;

theorem :: ORDERS_5:40
  for A being set, D being a_partition of A holds
    ERl D = EqRelOf PreorderFromPartition(D);

reserve X,Z for set;
reserve x,y,z for object;
reserve A,B,C for Subset of X;

theorem :: ORDERS_5:41
  for A being set, D being a_partition of A holds
    D = Class EqRelOf PreorderFromPartition(D);

theorem :: ORDERS_5:42
  for A being set, D being a_partition of A holds
    D = the carrier of QuotientOrder(PreorderFromPartition(D));

definition
  let A be set, D be a_partition of A, X be Element of D, f be Function;
  func eqSupport(f, X) -> Subset of A equals
:: ORDERS_5:def 11
  support f /\ X;
end;

definition
  let A be Preorder, X be Element of QuotientOrder(A),
  f be Function;
  func eqSupport(f, X) -> Subset of A means
:: ORDERS_5:def 12
  ex D being a_partition of the carrier of A, Y being Element of D st
  D = the carrier of QuotientOrder(A) & Y = X & it = eqSupport(f, Y);
end;

definition
  let A be Preorder, X be Element of QuotientOrder(A),
  f be Function;
  redefine func eqSupport(f, X) equals
:: ORDERS_5:def 13
  support f /\ X;
end;

registration
  let A be set, D be a_partition of A, f be finite-support Function,
  X be Element of D;
  cluster eqSupport(f, X) -> finite;
end;

registration
  let A be Preorder, f be finite-support Function,
  X be Element of QuotientOrder(A);
  cluster eqSupport(f, X) -> finite;
end;

registration
  let A be Order;
  let X be Element of the carrier of QuotientOrder(A);
  let f be finite-support Function of A, REAL;
  cluster eqSupport(f, X) -> trivial;
end;

theorem :: ORDERS_5:43
  for A being set, D being a_partition of A, X being Element of D,
    f being Function of A, REAL
  holds
    eqSupport(f, X) = eqSupport(-f, X);

theorem :: ORDERS_5:44
  for A being Preorder, X being Element of QuotientOrder(A),
    f being Function of A, REAL
  holds
    eqSupport(f, X) = eqSupport(-f, X);

definition
  let A be set, D be a_partition of A, f be finite-support Function of A, REAL;
  func D eqSumOf f -> Function of D, REAL means
:: ORDERS_5:def 14

  for X being Element of D st X in D holds
    it.X = Sum (f * (canFS (eqSupport(f, X))) );
end;

definition
  let A be Preorder, f be finite-support Function of A, REAL;
  func eqSumOf f -> Function of QuotientOrder(A), REAL means
:: ORDERS_5:def 15
  ex D being a_partition of the carrier of A st
  D = the carrier of QuotientOrder(A) & it = D eqSumOf f;
end;

definition
  let A be Preorder, f be finite-support Function of A, REAL;
  redefine func eqSumOf f means
:: ORDERS_5:def 16

  for X being Element of QuotientOrder(A) st X in the carrier of
    QuotientOrder(A) holds
      it.X = Sum (f * (canFS (eqSupport(f, X))) );
end;

theorem :: ORDERS_5:45
  for A being set, D being a_partition of A,
    f being finite-support Function of A, REAL
  holds
    (D eqSumOf -f) = -(D eqSumOf f);

theorem :: ORDERS_5:46
  for A being Preorder,
    f being finite-support Function of A, REAL
  holds
    eqSumOf -f = -eqSumOf f;

registration
  let A be Preorder,
      f be nonnegative-yielding finite-support Function of A, REAL;
  cluster eqSumOf f -> nonnegative-yielding;
end;

registration
  let A be set, D be a_partition of A;
  let f be nonnegative-yielding finite-support Function of A, REAL;
  cluster D eqSumOf f -> nonnegative-yielding;
end;

theorem :: ORDERS_5:47
  for A being set, D being a_partition of A,
    f being finite-support Function of A, REAL
      st f is nonpositive-yielding
  holds
    D eqSumOf f is nonpositive-yielding;

theorem :: ORDERS_5:48
  for A being Preorder, f being finite-support Function of A, REAL
    st f is nonpositive-yielding
  holds
    eqSumOf f is nonpositive-yielding;

theorem :: ORDERS_5:49
  for A being Preorder, f being finite-support Function of A, REAL,
    x being Element of A st
      (for y being Element of A st x =~ y holds x = y) holds
    ((eqSumOf f)*(proj A)).x = f.x;

theorem :: ORDERS_5:50
  for A being Order, f being finite-support Function of A, REAL holds
    (eqSumOf f)*(proj A) = f;

theorem :: ORDERS_5:51
  for A being Order, f1, f2 being finite-support Function of A, REAL holds
    eqSumOf f1 = eqSumOf f2 implies f1 = f2;

theorem :: ORDERS_5:52
  for A being Preorder,
    f being finite-support Function of A, REAL
  holds
    support eqSumOf f c= (proj A).:support f;

theorem :: ORDERS_5:53
  for A being non empty set, D being non empty a_partition of A,
    f being finite-support Function of A, REAL
  holds
    support (D eqSumOf f) c= (proj D).:support f;

:: more general:
::  for x holds (for y in (proj A).x holds f.y >= 0) or
::    (for y in (proj A).x holds f.y <= 0)
theorem :: ORDERS_5:54
  for A being Preorder,
    f being finite-support Function of A, REAL
  st
    f is nonnegative-yielding
  holds
    (proj A).:support f = support eqSumOf f;

theorem :: ORDERS_5:55
  for A being non empty set, D being non empty a_partition of A,
    f being finite-support Function of A, REAL
  st
    f is nonnegative-yielding
  holds
    (proj D).:support f = support (D eqSumOf f);

theorem :: ORDERS_5:56
  for A being Preorder,
    f being finite-support Function of A, REAL
  st
    f is nonpositive-yielding
  holds
    (proj A).:support f = support eqSumOf f;

theorem :: ORDERS_5:57
  for A being non empty set, D being non empty a_partition of A,
    f being finite-support Function of A, REAL
  st
    f is nonpositive-yielding
  holds
    (proj D).:support f = support (D eqSumOf f);

registration
  let A be Preorder,
      f be finite-support Function of A, REAL;
  cluster eqSumOf f -> finite-support;
end;

registration
  let A be set, D be a_partition of A,
  f be finite-support Function of A, REAL;
  cluster D eqSumOf f -> finite-support;
end;

theorem :: ORDERS_5:58
  for A being non empty set, D being non empty a_partition of A,
    f being finite-support Function of A, REAL,
    s1 being one-to-one FinSequence of A,
    s2 being one-to-one FinSequence of D
  st
    rng s2 = (proj D).:rng s1 &
    (for X being Element of D st X in rng s2 holds eqSupport(f, X) c= rng s1)
  holds
    Sum((D eqSumOf f) * s2) = Sum(f * s1);

theorem :: ORDERS_5:59
  for A being non empty set, D being non empty a_partition of A,
    f being finite-support Function of A, REAL,
    s1 being one-to-one FinSequence of A,
    s2 being one-to-one FinSequence of D
  st
    rng s1 = support f & rng s2 = support(D eqSumOf f)
  holds
    Sum((D eqSumOf f) * s2) = Sum(f * s1);

theorem :: ORDERS_5:60
  for A being Preorder, f being finite-support Function of A, REAL,
    s1 being one-to-one FinSequence of A,
    s2 being one-to-one FinSequence of QuotientOrder(A)
  st
    rng s1 = support f & rng s2 = support (eqSumOf f)
  holds
    Sum((eqSumOf f)*s2) = Sum(f*s1);

begin :: Ordering Finite Sequences

definition
  let A be RelStr;
  let s be FinSequence of A;
  attr s is weakly-ascending means
:: ORDERS_5:def 17
  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.n <= s/.m;
end;

definition
  let A be RelStr;
  let s be FinSequence of A;
  attr s is ascending means
:: ORDERS_5:def 18
  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.n <~ s/.m;
end;

:: it is surprising that this isn't a trivial proof by Def4
registration
  let A be RelStr;
  cluster ascending -> weakly-ascending for FinSequence of A;
end;

definition
  let A be antisymmetric RelStr;
  let s be FinSequence of A;
  redefine attr s is ascending means
:: ORDERS_5:def 19

  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.n < s/.m;
end;

definition
  let A be RelStr;
  let s be FinSequence of A;
  attr s is weakly-descending means
:: ORDERS_5:def 20
  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.m <= s/.n;
end;

definition
  let A be RelStr;
  let s be FinSequence of A;
  attr s is descending means
:: ORDERS_5:def 21
  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.m <~ s/.n;
end;

registration
  let A be RelStr;
  cluster descending -> weakly-descending for FinSequence of A;
end;

definition
  let A be antisymmetric RelStr;
  let s be FinSequence of A;
  redefine attr s is descending means
:: ORDERS_5:def 22
  for n,m being Nat st n in dom s & m in dom s & n < m holds
    s/.m < s/.n;
end;

registration
  let A be antisymmetric RelStr;
  cluster one-to-one weakly-ascending -> ascending for FinSequence of A;
  cluster one-to-one weakly-descending -> descending for FinSequence of A;
end;

registration
  let A be antisymmetric RelStr;
  cluster weakly-ascending weakly-descending -> constant for FinSequence of A;
end;

registration
  let A be reflexive RelStr;
  cluster constant -> weakly-ascending weakly-descending for FinSequence of A;
end;

registration
  let A be RelStr;
  cluster <*>the carrier of A -> ascending weakly-ascending
    descending weakly-descending;
end;

registration
  let A be RelStr;
  cluster empty ascending weakly-ascending descending weakly-descending
    for FinSequence of A;
end;

registration
  let A be non empty RelStr;
  let x be Element of A;
  cluster <* x *> -> ascending weakly-ascending
    descending weakly-descending for FinSequence of A;
end;

registration
  let A be non empty RelStr;
  cluster non empty one-to-one ascending weakly-ascending
    descending weakly-descending for FinSequence of A;
end;

definition
  let A be RelStr;
  let s be FinSequence of A;
  attr s is asc_ordering means
:: ORDERS_5:def 23
  s is one-to-one & s is weakly-ascending;
  attr s is desc_ordering means
:: ORDERS_5:def 24
  s is one-to-one & s is weakly-descending;
end;

registration
  let A be RelStr;
  cluster asc_ordering -> one-to-one weakly-ascending for FinSequence of A;
  cluster one-to-one weakly-ascending -> asc_ordering for FinSequence of A;
  cluster desc_ordering -> one-to-one weakly-descending for FinSequence of A;
  cluster one-to-one weakly-descending -> desc_ordering for FinSequence of A;
end;

:: I thought the following registration would only work with trasitivity
:: but apparently ascending implies asc_ordering
registration
  let A be RelStr;
  cluster ascending -> asc_ordering for FinSequence of A;
  cluster descending -> desc_ordering for FinSequence of A;
end;

definition
  let A be RelStr;
  let B be Subset of A;
  let s be FinSequence of A;
  attr s is B-asc_ordering means
:: ORDERS_5:def 25
  s is asc_ordering & rng s = B;
  attr s is B-desc_ordering means
:: ORDERS_5:def 26
  s is desc_ordering & rng s = B;
end;

registration
  let A be RelStr, B be Subset of A;
  cluster B-asc_ordering -> asc_ordering for FinSequence of A;
  cluster B-desc_ordering -> desc_ordering for FinSequence of A;
end;

registration
  let A be RelStr, B be empty Subset of A;
  cluster B-asc_ordering -> empty for FinSequence of A;
  cluster B-desc_ordering -> empty for FinSequence of A;
end;

theorem :: ORDERS_5:61
  for A being RelStr, s being FinSequence of A holds
    s is weakly-ascending iff Rev(s) is weakly-descending;

theorem :: ORDERS_5:62
  for A being RelStr, s being FinSequence of A holds
    s is ascending iff Rev(s) is descending;

theorem :: ORDERS_5:63
  for A being RelStr, B being Subset of A, s being FinSequence of A holds
    s is B-asc_ordering iff Rev(s) is B-desc_ordering;

:: this seems trivial, I'm unsure why
theorem :: ORDERS_5:64
  for A being RelStr, B being Subset of A,
    s being FinSequence of A holds
      s is B-asc_ordering or s is B-desc_ordering implies B is finite;

registration
  let A be antisymmetric RelStr;
  cluster asc_ordering -> ascending for FinSequence of A;
  cluster desc_ordering -> descending for FinSequence of A;
end;

theorem :: ORDERS_5:65
  for A being antisymmetric RelStr, B being Subset of A,
    s1, s2 being FinSequence of A st
      s1 is B-asc_ordering & s2 is B-asc_ordering holds s1 = s2;

theorem :: ORDERS_5:66
  for A being antisymmetric RelStr, B being Subset of A,
    s1, s2 being FinSequence of A st
      s1 is B-desc_ordering & s2 is B-desc_ordering holds s1 = s2;

theorem :: ORDERS_5:67
  for A being LinearOrder, B being finite Subset of A,
    s being FinSequence of A holds
      s is B-asc_ordering iff s = SgmX(the InternalRel of A, B);

registration
  let A be LinearOrder, B be finite Subset of A;
  cluster SgmX(the InternalRel of A, B) -> B-asc_ordering;
end;

theorem :: ORDERS_5:68
  for A being RelStr, B, C being Subset of A,
    s being FinSequence of A
      st s is B-asc_ordering & C c= B
    holds
      ex s2 being FinSequence of A st s2 is C-asc_ordering;

theorem :: ORDERS_5:69
  for A being RelStr, B, C being Subset of A,
    s being FinSequence of A
  st s is B-desc_ordering & C c= B holds
    ex s2 being FinSequence of A st s2 is C-desc_ordering;

theorem :: ORDERS_5:70
  for A being RelStr, B being Subset of A,
    s being FinSequence of A, x being Element of A
  st B = {x} & s = <*x*> holds
    s is B-asc_ordering & s is B-desc_ordering;

theorem :: ORDERS_5:71
  for A being RelStr, B being Subset of A, s being FinSequence of A
    st s is B-asc_ordering holds
      the InternalRel of A is_connected_in B;

theorem :: ORDERS_5:72
  for A being RelStr, B being Subset of A, s being FinSequence of A
    st s is B-desc_ordering holds
      the InternalRel of A is_connected_in B;

theorem :: ORDERS_5:73
  for A being transitive RelStr, B, C being Subset of A,
    s1 being FinSequence of A, x being Element of A
  st
    s1 is C-asc_ordering & not x in C & B = C \/ {x} &
      for y being Element of A st y in C holds x <= y
  holds
    ex s2 being FinSequence of A st
      s2 = <*x*> ^ s1 & s2 is B-asc_ordering;

theorem :: ORDERS_5:74
  for A being transitive RelStr, B, C being Subset of A,
      s1 being FinSequence of A, x being Element of A
  st s1 is C-asc_ordering & not x in C & B = C \/ {x} &
    for y being Element of A st y in C holds y <= x
  holds ex s2 being FinSequence of A st
    s2 = s1 ^ <*x*> & s2 is B-asc_ordering;

theorem :: ORDERS_5:75
  for A being transitive RelStr, B, C being Subset of A,
    s1 being FinSequence of A, x being Element of A
  st s1 is C-desc_ordering & not x in C & B = C \/ {x} &
    for y being Element of A st y in C holds x <= y
  holds
    ex s2 being FinSequence of A st
      s2 = s1 ^ <*x*> & s2 is B-desc_ordering;

theorem :: ORDERS_5:76
  for A being transitive RelStr, B, C being Subset of A,
    s1 being FinSequence of A, x being Element of A
  st s1 is C-desc_ordering & not x in C & B = C \/ {x} &
    for y being Element of A st y in C holds y <= x
  holds
    ex s2 being FinSequence of A st
      s2 = <*x*> ^ s1 & s2 is B-desc_ordering;

theorem :: ORDERS_5:77
  for A being transitive RelStr, B being finite Subset of A st
    the InternalRel of A is_connected_in B holds
      ex s being FinSequence of A st s is B-asc_ordering;

theorem :: ORDERS_5:78
  for A being transitive RelStr, B being finite Subset of A st
    the InternalRel of A is_connected_in B holds
      ex s being FinSequence of A st s is B-desc_ordering;

theorem :: ORDERS_5:79
  for A being connected transitive RelStr, B being finite Subset of A holds
    ex s being FinSequence of A st s is B-asc_ordering;

theorem :: ORDERS_5:80
  for A being connected transitive RelStr, B being finite Subset of A holds
    ex s being FinSequence of A st s is B-desc_ordering;

registration
  let A be connected transitive RelStr;
  let B be finite Subset of A;
  cluster B-asc_ordering for FinSequence of A;
  cluster B-desc_ordering for FinSequence of A;
end;

theorem :: ORDERS_5:81
  for A being Preorder, B being Subset of A st
      the InternalRel of A is_connected_in B
    holds
      the InternalRel of QuotientOrder(A) is_connected_in (proj A).:B;

theorem :: ORDERS_5:82
  for A being Preorder, B being Subset of A,
    s1 being FinSequence of A
  st
    s1 is B-asc_ordering
  holds
    ex s2 being FinSequence of QuotientOrder(A) st
      s2 is ((proj A).:B)-asc_ordering;

theorem :: ORDERS_5:83
  for A being Preorder, B being Subset of A,
    s1 being FinSequence of A
  st
    s1 is B-desc_ordering
  holds
    ex s2 being FinSequence of QuotientOrder(A) st
      s2 is ((proj A).:B)-desc_ordering;