:: Order Sorted Algebras
::  by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2012 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 PBOOLE, FINSEQ_1, RELAT_1, TARSKI, XBOOLE_0, MSUALG_1, SUBSET_1,
      STRUCT_0, EQREL_1, FUNCT_1, ORDERS_2, ORDERS_1, RELAT_2, NATTRA_1,
      MARGREL1, XXREAL_0, SEQM_3, CARD_5, CARD_LAR, FUNCOP_1, CARD_3, SETFAM_1,
      OSALG_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1,
      ORDERS_1, FUNCT_2, EQREL_1, SETFAM_1, PARTFUN1, FINSEQ_1, FUNCOP_1,
      FINSEQ_2, CARD_3, PBOOLE, ORDERS_2, STRUCT_0, MSUALG_1, ORDERS_3;
 constructors EQREL_1, ORDERS_3, RELSET_1, MSAFREE;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1,
      STRUCT_0, MSUALG_1, ORDERS_3, ORDINAL1, RELAT_1, PBOOLE, FINSEQ_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI;
 theorems FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, PBOOLE, FUNCT_2, CARD_3,
      FINSEQ_3, FINSEQ_2, RELAT_1, RELSET_1, EQREL_1, ZFMISC_1, ORDERS_3,
      MSUALG_1, ORDERS_2, RELAT_2, GRFUNC_1, FUNCT_4, ORDERS_1, XTUPLE_0;
 schemes FUNCT_1;

begin :: Preliminaries
:: TODO: constant ManySortedSet, constant OrderSortedSet,
:: constant -> order-sorted ManySortedSet of R

registration
  let I be set, f be ManySortedSet of I, p be FinSequence of I;
  cluster f * p -> FinSequence-like;
  coherence
  proof
    rng p c= I;
    then rng p c= dom f by PARTFUN1:def 2;
    then dom(f*p) = dom p by RELAT_1:27
      .= Seg len p by FINSEQ_1:def 3;
    hence thesis by FINSEQ_1:def 2;
  end;
end;

Lm1: for I being set, f being ManySortedSet of I, p being FinSequence of I
holds dom (f * p) = dom p & len (f * p) = len p
proof
  let I be set, f be ManySortedSet of I, p be FinSequence of I;
  reconsider q = f * p as FinSequence;
  rng p c= I;
  then rng p c= dom f by PARTFUN1:def 2;
  then len q = len p by FINSEQ_2:29;
  hence thesis by FINSEQ_3:29;
end;

definition
  let S be non empty ManySortedSign;
  mode SortSymbol of S is Element of S;
end;

definition
  let S be non empty ManySortedSign;
  mode OperSymbol of S is Element of the carrier' of S;
end;

:: Some structures
:: overloaded MSALGEBRA is modelled using an Equivalence_Relation
:: on carrier' ... partially hack enforced by previous articles,
:: partially can give more general treatment than the usual definition

definition
  struct(ManySortedSign) OverloadedMSSign (# carrier -> set, carrier' -> set,
Overloading -> Equivalence_Relation of the carrier', Arity -> Function of the
carrier', the carrier*, ResultSort -> Function of the carrier', the carrier #);
end;

:: Order Sorted Signatures

definition
  struct(ManySortedSign,RelStr) RelSortedSign (# carrier -> set, InternalRel
    -> (Relation of the carrier), carrier' -> set, Arity -> Function of the
carrier', the carrier*, ResultSort -> Function of the carrier', the carrier #);
end;

definition
  struct(OverloadedMSSign,RelSortedSign) OverloadedRSSign (# carrier -> set,
    InternalRel -> (Relation of the carrier), carrier' -> set, Overloading ->
Equivalence_Relation of the carrier', Arity -> Function of the carrier', the
    carrier*, ResultSort -> Function of the carrier', the carrier #);
end;

:: The inheritance for structures should be much improved, much of the
:: following is very bad hacking

reserve A,O for non empty set,
  R for Order of A,
  Ol for Equivalence_Relation of O,
  f for Function of O,A*,
  g for Function of O,A;

:: following should be possible, but isn't:
:: set RS0 = RelSortedSign(#A,R,O,f,g #);
:: inheritance of attributes for structures does not work!!! :
:: RelStr(#A,R#) is reflexive does not imply that for RelSortedSign(...)

theorem Th1:
  OverloadedRSSign(#A,R,O,Ol,f,g #) is non empty non void reflexive
  transitive antisymmetric
proof
  set RS0 = OverloadedRSSign(#A,R,O,Ol,f,g #);
A1: field the InternalRel of RS0 = the carrier of RS0 by ORDERS_1:12;
  then
A2: the InternalRel of RS0 is_antisymmetric_in the carrier of RS0 by
RELAT_2:def 12;
  the InternalRel of RS0 is_reflexive_in the carrier of RS0 & the
InternalRel of RS0 is_transitive_in the carrier of RS0 by A1,RELAT_2:def 9
,def 16;
  hence thesis by A2,ORDERS_2:def 2,def 3,def 4;
end;

registration
  let A,R,O,Ol,f,g;
  cluster OverloadedRSSign(#A,R,O,Ol,f,g #) -> strict non empty reflexive
    transitive antisymmetric;
  coherence by Th1;
end;

begin

::   order-sorted, ~=, discernable,  op-discrete

reserve S for OverloadedRSSign;

:: should be stated for nonoverloaded, but the inheritance is bad

definition
  let S;

  attr S is order-sorted means
  :Def1:
  S is reflexive transitive antisymmetric;
end;

registration
  cluster order-sorted -> reflexive transitive antisymmetric for
OverloadedRSSign;
  coherence by Def1;
  cluster strict non empty non void order-sorted for OverloadedRSSign;
  existence
  proof

set A = the non empty set,R = the Order of A,O = the non empty set,Ol =the
Equivalence_Relation of O,f = the Function of O,A*,g = the Function of O,A;
    take OverloadedRSSign(#A,R,O,Ol,f,g #);
    thus thesis by Def1;
  end;
end;

registration
  cluster non empty non void for OverloadedMSSign;
  existence
  proof
    set X = the non empty non void OverloadedRSSign;
    take X;
    thus thesis;
  end;
end;

definition
  let S be non empty non void OverloadedMSSign;
  let x,y be OperSymbol of S;
  pred x ~= y means
  :Def2:
  [x,y] in the Overloading of S;
  symmetry
  proof
    let x,y be OperSymbol of S;
    field the Overloading of S = the carrier' of S by ORDERS_1:12;
    then the Overloading of S is_symmetric_in the carrier' of S by
RELAT_2:def 11;
    hence thesis by RELAT_2:def 3;
  end;
  reflexivity
  proof
    let x be OperSymbol of S;
    field the Overloading of S = the carrier' of S by ORDERS_1:12;
    then the Overloading of S is_reflexive_in the carrier' of S by
RELAT_2:def 9;
    hence thesis by RELAT_2:def 1;
  end;
end;

:: remove when transitivity implemented

theorem Th2:
  for S being non empty non void OverloadedMSSign, o,o1,o2 being
  OperSymbol of S holds o ~= o1 & o1 ~= o2 implies o ~= o2
proof
  let S be non empty non void OverloadedMSSign;
  let o,o1,o2 be OperSymbol of S;
  field the Overloading of S = the carrier' of S by ORDERS_1:12;
  then
A1: the Overloading of S is_transitive_in the carrier' of S by RELAT_2:def 16;
  assume o ~= o1 & o1 ~= o2;
  then [o,o1] in the Overloading of S & [o1,o2] in the Overloading of S by Def2
;
  then [o,o2] in the Overloading of S by A1,RELAT_2:def 8;
  hence thesis by Def2;
end;

:: with previous definition, equivalent funcs with same rank could exist

definition
  let S be non empty non void OverloadedMSSign;
  attr S is discernable means
  :Def3:
  for x,y be OperSymbol of S st x ~= y &
  the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y
  holds x = y;
  attr S is op-discrete means
  :Def4:
  the Overloading of S = id (the carrier' of S);
end;

theorem Th3:
  for S being non empty non void OverloadedMSSign holds S is
  op-discrete iff for x,y be OperSymbol of S st x ~= y holds x = y
proof
  let S be non empty non void OverloadedMSSign;
  set d = id the carrier' of S;
  set opss = the carrier' of S;
  set ol = the Overloading of S;
  thus S is op-discrete implies for x,y be OperSymbol of S st x ~= y holds x =
  y
  proof
    assume
A1: S is op-discrete;
    let x,y be OperSymbol of S;
    assume x ~= y;
    then [x,y] in the Overloading of S by Def2;
    then [x,y] in d by A1,Def4;
    hence thesis by RELAT_1:def 10;
  end;
  assume
A2: for x,y be OperSymbol of S st x ~= y holds x = y;
  now
    let x,y be set;
    thus [x,y] in ol implies x in opss & x = y
    proof
      assume
A3:   [x,y] in ol;
      then ex x1,y1 being set st [x,y] = [x1,y1] & x1 in opss & y1 in opss by
RELSET_1:2;
      then reconsider x2 = x, y2 = y as OperSymbol of S by XTUPLE_0:1;
      x2 ~= y2 by A3,Def2;
      hence thesis by A2;
    end;
    assume x in opss & x = y;
    hence [x,y] in ol by Def2;
  end;
  hence the Overloading of S = d by RELAT_1:def 10;
end;

theorem Th4:
  for S being non empty non void OverloadedMSSign holds S is
  op-discrete implies S is discernable
proof
  let S be non empty non void OverloadedMSSign;
  assume
A1: S is op-discrete;
  let x,y be OperSymbol of S;
  thus thesis by A1,Th3;
end;

begin

:: OSSign of ManySortedSign, OrderSortedSign

reserve S0 for non empty non void ManySortedSign;

:: we require strictness here for simplicity, more interesting is whether
:: we could do a nonstrict version, keeping the remaining fields of S0;

definition
  let S0;
  func OSSign S0 -> strict non empty non void order-sorted OverloadedRSSign
  means
  :Def5:
  the carrier of S0 = the carrier of it & id the carrier of S0 = the
  InternalRel of it & the carrier' of S0 = the carrier' of it & id the carrier'
  of S0 = the Overloading of it & the Arity of S0 = the Arity of it & the
  ResultSort of S0 = the ResultSort of it;
  existence
  proof
    set s = OverloadedRSSign(# the carrier of S0, id the carrier of S0, the
carrier' of S0, id the carrier' of S0, the Arity of S0, the ResultSort of S0 #)
    ;
    reconsider s1 = s as strict non empty non void order-sorted
    OverloadedRSSign by Def1;
    take s1;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th5:
  OSSign S0 is discrete op-discrete
proof
  set s = OSSign S0;
  set ol = the Overloading of s;
  the carrier of S0 = the carrier of OSSign S0 & id the carrier of S0 =
  the InternalRel of OSSign S0 by Def5;
  hence OSSign S0 is discrete by ORDERS_3:def 1;
A1: the Overloading of OSSign S0 = id the carrier' of S0 by Def5;
  now
    let x,y be OperSymbol of s;
    assume x ~= y;
    then [x,y] in ol by Def2;
    hence x = y by A1,RELAT_1:def 10;
  end;
  hence thesis by Th3;
end;

registration
  cluster discrete op-discrete discernable for strict non empty non void
    order-sorted OverloadedRSSign;
  existence
  proof
    set S0 = the non empty non void ManySortedSign;
    take s = OSSign S0;
    thus s is discrete op-discrete by Th5;
    hence thesis by Th4;
  end;
end;

registration
  cluster op-discrete -> discernable for non empty non void OverloadedRSSign;
  coherence by Th4;
end;

::FIXME: the order of this and the previous clusters cannot be exchanged!!

registration
  let S0;
  cluster OSSign S0 -> discrete op-discrete;
  coherence by Th5;
end;

definition
  mode OrderSortedSign is discernable non empty non void order-sorted
    OverloadedRSSign;
end;

:: monotonicity of OrderSortedSign
:: monotone overloaded signature means monotonicity for equivalent
:: operations
:: a stronger property of the Overloading should be stated ...
:: o1 ~= o2 implies len (the_arity_of o2) = len (the_arity_of o1)
:: ... probably not, unnecessary

reserve S for non empty Poset;
reserve s1,s2 for Element of S;
reserve w1,w2 for Element of (the carrier of S)*;

:: this is mostly done in YELLOW_1, but getting the constructors work
:: could be major effort;  I don't care now

definition
  let S;
  let w1,w2 be Element of (the carrier of S)*;
  pred w1 <= w2 means
  :Def6:
  len w1 = len w2 & for i being set st i in dom w1
  for s1,s2 st s1 = w1.i & s2 = w2.i holds s1 <= s2;
  reflexivity;
end;

theorem Th6:
  for w1,w2 being Element of (the carrier of S)* holds w1 <= w2 &
  w2 <= w1 implies w1 = w2
proof
  let w1,w2 be Element of (the carrier of S)*;
  assume that
A1: w1 <= w2 and
A2: w2 <= w1;
  len w1 = len w2 by A1,Def6;
  then
A3: dom w1 = dom w2 by FINSEQ_3:29;
  for i being set st i in dom w1 holds w1.i = w2.i
  proof
    let i be set such that
A4: i in dom w1;
    reconsider s3 = w1.i, s4 = w2.i as Element of S by A3,A4,PARTFUN1:4;
    s3 <= s4 & s4 <= s3 by A1,A2,A3,A4,Def6;
    hence thesis by ORDERS_2:2;
  end;
  hence thesis by A3,FUNCT_1:2;
end;

theorem Th7:
  S is discrete & w1 <= w2 implies w1 = w2
proof
  assume that
A1: S is discrete and
A2: w1 <= w2;
  reconsider S1 = S as discrete non empty Poset by A1;
  len w1 = len w2 by A2,Def6;
  then
A3: dom w1 = dom w2 by FINSEQ_3:29;
  for i being set st i in dom w1 holds w1.i = w2.i
  proof
    let i be set such that
A4: i in dom w1;
    reconsider s3 = w1.i, s4 = w2.i as Element of S by A3,A4,PARTFUN1:4;
    reconsider s5 = s3, s6 = s4 as Element of S1;
    s3 <= s4 by A2,A4,Def6;
    then s5 = s6 by ORDERS_3:1;
    hence thesis;
  end;
  hence thesis by A3,FUNCT_1:2;
end;

reserve S for OrderSortedSign;
reserve o,o1,o2 for OperSymbol of S;
reserve w1 for Element of (the carrier of S)*;

theorem Th8:
  S is discrete & o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2)
  & the_result_sort_of o1 <= the_result_sort_of o2 implies o1 = o2
proof
  assume
A1: S is discrete;
  then reconsider S1 = S as discrete OrderSortedSign;
  reconsider s1 = the_result_sort_of o1, s2 = the_result_sort_of o2 as
  SortSymbol of S1;
  assume that
A2: o1 ~= o2 and
A3: (the_arity_of o1) <= (the_arity_of o2) and
A4: the_result_sort_of o1 <= the_result_sort_of o2;
A5: s1 = s2 by A4,ORDERS_3:1;
  (the_arity_of o1) = (the_arity_of o2) by A1,A3,Th7;
  hence thesis by A2,A5,Def3;
end;

:: monotonicity of the signature
:: this doesnot extend to Overloading!

definition
  let S;
  let o;
  attr o is monotone means
  :Def7:
  for o2 st o ~= o2 & (the_arity_of o) <= (
  the_arity_of o2) holds the_result_sort_of o <= the_result_sort_of o2;
end;

definition
  let S;
  attr S is monotone means
  :Def8:
  for o being OperSymbol of S holds o is monotone;
end;

theorem Th9:
  S is op-discrete implies S is monotone
proof
  set ol = the Overloading of S;
  assume S is op-discrete;
  then
A1: ol = id the carrier' of S by Def4;
  let o be OperSymbol of S;
  let o2 be OperSymbol of S;
  assume o ~= o2;
  then [o,o2] in ol by Def2;
  hence thesis by A1,RELAT_1:def 10;
end;

registration
  cluster monotone for OrderSortedSign;
  existence
  proof
    set S = the op-discrete OrderSortedSign;
    take S;
    thus thesis by Th9;
  end;
end;

registration
  let S be monotone OrderSortedSign;
  cluster monotone for OperSymbol of S;
  existence
  proof
    set o = the OperSymbol of S;
    take o;
    thus thesis by Def8;
  end;
end;

registration
  let S be monotone OrderSortedSign;
  cluster -> monotone for OperSymbol of S;
  coherence by Def8;
end;

registration
  cluster op-discrete -> monotone for OrderSortedSign;
  coherence by Th9;
end;

theorem :: constants not overloaded if monotone
  S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {}
  implies o1=o2
proof
  assume that
A1: S is monotone and
A2: the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {};
  the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2
  <= the_result_sort_of o1 by A1,A2,Def7;
  then the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
  hence thesis by A2,Def3;
end;

:: least args,sort,rank,regularity for OperSymbol and
:: monotone OrderSortedSign
:: least bound for arguments

definition
  let S,o,o1,w1;
  pred o1 has_least_args_for o,w1 means
  :Def9:
  o ~= o1 & w1 <= the_arity_of
  o1 & for o2 st o ~= o2 & w1 <= the_arity_of o2 holds the_arity_of o1 <=
  the_arity_of o2;
  pred o1 has_least_sort_for o,w1 means
  :Def10:
  o ~= o1 & w1 <= the_arity_of
  o1 & for o2 st o ~= o2 & w1 <= the_arity_of o2 holds the_result_sort_of o1 <=
  the_result_sort_of o2;
end;

definition
  let S,o,o1,w1;
  pred o1 has_least_rank_for o,w1 means
  :Def11:
  o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1;
end;

definition
  let S,o;
  attr o is regular means
  :Def12:
  o is monotone & for w1 st w1 <= the_arity_of
  o ex o1 st o1 has_least_args_for o,w1;
end;

definition
  let SM be monotone OrderSortedSign;
  attr SM is regular means
  :Def13:
  for om being OperSymbol of SM holds om is regular;
end;

reserve SM for monotone OrderSortedSign,
  o,o1,o2 for OperSymbol of SM,
  w1 for Element of (the carrier of SM)*;

theorem Th11:
  SM is regular iff for o,w1 st w1 <= the_arity_of o ex o1 st o1
  has_least_rank_for o,w1
proof
  hereby
    assume
A1: SM is regular;
    let o,w1;
    assume
A2: w1 <= the_arity_of o;
    o is regular by A1,Def13;
    then consider o1 such that
A3: o1 has_least_args_for o,w1 by A2,Def12;
    take o1;
    o1 has_least_sort_for o,w1
    proof
      thus
A4:   o ~= o1 & w1 <= the_arity_of o1 by A3,Def9;
      let o2;
      assume that
A5:   o ~= o2 and
A6:   w1 <= the_arity_of o2;
A7:   o1 ~= o2 by A4,A5,Th2;
      the_arity_of o1 <= the_arity_of o2 by A3,A5,A6,Def9;
      hence thesis by A7,Def7;
    end;
    hence o1 has_least_rank_for o,w1 by A3,Def11;
  end;
  assume
A8: for o,w1 st w1 <= the_arity_of o ex o1 st o1 has_least_rank_for o, w1;
  let o;
  thus o is monotone;
  let w1;
  assume w1 <= the_arity_of o;
  then consider o1 such that
A9: o1 has_least_rank_for o,w1 by A8;
  take o1;
  thus thesis by A9,Def11;
end;

theorem Th12:
  for SM being monotone OrderSortedSign holds SM is op-discrete
  implies SM is regular
proof
  let SM be monotone OrderSortedSign;
  assume
A1: SM is op-discrete;
  let om be OperSymbol of SM;
  thus om is monotone;
  let wm1 be Element of (the carrier of SM)* such that
A2: wm1 <= the_arity_of om;
  om has_least_args_for om,wm1
  proof
    thus om ~= om & wm1 <= the_arity_of om by A2;
    let om2 be OperSymbol of SM;
    assume that
A3: om ~= om2 and
    wm1 <= the_arity_of om2;
    thus thesis by A1,A3,Th3;
  end;
  hence thesis;
end;

registration
  cluster regular for monotone OrderSortedSign;
  existence
  proof
    set SM = the op-discrete OrderSortedSign;
    take SM;
    thus thesis by Th12;
  end;
end;

registration
  cluster op-discrete -> regular for monotone OrderSortedSign;
  coherence by Th12;
end;

registration
  let SR be regular monotone OrderSortedSign;
  cluster -> regular for OperSymbol of SR;
  coherence by Def13;
end;

reserve SR for regular monotone OrderSortedSign,
  o,o1,o3,o4 for OperSymbol of SR,
  w1 for Element of (the carrier of SR)*;

theorem Th13:
  o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 implies o3 = o4
proof
  assume that
A1: o3 has_least_args_for o,w1 and
A2: o4 has_least_args_for o,w1;
A3: o ~= o3 by A1,Def9;
A4: o ~= o4 by A2,Def9;
  then
A5: o3 ~= o4 by A3,Th2;
  w1 <= the_arity_of o3 by A1,Def9;
  then
A6: the_arity_of o4 <= the_arity_of o3 by A2,A3,Def9;
  then
A7: the_result_sort_of o4 <= the_result_sort_of o3 by A5,Def7;
  w1 <= the_arity_of o4 by A2,Def9;
  then
A8: the_arity_of o3 <= the_arity_of o4 by A1,A4,Def9;
  then
A9: the_arity_of o3 = the_arity_of o4 by A6,Th6;
  the_result_sort_of o3 <= the_result_sort_of o4 by A5,A8,Def7;
  then the_result_sort_of o3 = the_result_sort_of o4 by A7,ORDERS_2:2;
  hence thesis by A5,A9,Def3;
end;

definition
  let SR,o,w1;
  assume
A1: w1 <= the_arity_of o;
  func LBound(o,w1) -> OperSymbol of SR means
  :Def14:
  it has_least_args_for o, w1;
  existence by A1,Def12;
  uniqueness by Th13;
end;

theorem Th14:
  for w1 st w1 <= the_arity_of o holds LBound(o,w1) has_least_rank_for o,w1
proof
  let w1;
  assume
A1: w1 <= the_arity_of o;
  then consider o1 such that
A2: o1 has_least_rank_for o,w1 by Th11;
  o1 has_least_args_for o,w1 by A2,Def11;
  hence thesis by A1,A2,Def14;
end;

:: ConstOSSet of Poset, OrderSortedSets

reserve R for non empty Poset;
reserve z for non empty set;

:: just to avoid on-the-spot casting in the examples

definition
  let R,z;
  func ConstOSSet(R,z) -> ManySortedSet of the carrier of R equals
  (the
  carrier of R) --> z;
  correctness
  proof
    the carrier of R = dom ((the carrier of R) --> z) by FUNCT_2:def 1;
    hence thesis by PARTFUN1:def 2;
  end;
end;

theorem Th15:
  ConstOSSet(R,z) is non-empty & for s1,s2 being Element of R st
  s1 <= s2 holds ConstOSSet(R,z).s1 c= ConstOSSet(R,z).s2
proof
  set x = ConstOSSet(R,z);
  set D = (the carrier of R) --> z;
  for s being set st s in the carrier of R holds x.s is non empty by FUNCOP_1:7
;
  hence x is non-empty by PBOOLE:def 13;
  let s1,s2 being Element of R;
  D.s1 = z by FUNCOP_1:7
    .= D.s2 by FUNCOP_1:7;
  hence thesis;
end;

definition
  let R;
  let M be ManySortedSet of R;

  attr M is order-sorted means
  :Def16:
  for s1,s2 being Element of R st s1 <= s2 holds M.s1 c= M.s2;
end;

theorem Th16:
  ConstOSSet(R,z) is order-sorted
proof
  set x = ConstOSSet(R,z);
  for s1,s2 being Element of R st s1 <= s2 holds x.s1 c= x.s2 by Th15;
  hence thesis by Def16;
end;

registration
  let R;
  cluster order-sorted for ManySortedSet of R;
  existence
  proof
    set z = the non empty set;
    take ConstOSSet(R,z);
    thus thesis by Th16;
  end;
end;

registration
  let R,z;
  cluster ConstOSSet(R,z) -> order-sorted;
  coherence by Th16;
end;

definition
  let R be non empty Poset;
  mode OrderSortedSet of R is order-sorted ManySortedSet of R;
end;

registration
  let R be non empty Poset;
  cluster non-empty for OrderSortedSet of R;
  existence
  proof
    take ConstOSSet(R,1);
    thus thesis by Th15;
  end;
end;

reserve s1,s2 for SortSymbol of S,
  o,o1,o2,o3 for OperSymbol of S,
  w1,w2 for Element of (the carrier of S)*;

definition
  let S;
  let M be MSAlgebra over S;
  attr M is order-sorted means
  :Def17:
  for s1,s2 st s1 <= s2 holds (the Sorts of M).s1 c= (the Sorts of M).s2;
end;

theorem Th17:
  for M being MSAlgebra over S holds M is order-sorted iff the
  Sorts of M is OrderSortedSet of S
proof
  let M be MSAlgebra over S;
  set So = the Sorts of M;
  reconsider So1 = So as ManySortedSet of S;
  thus M is order-sorted implies So is OrderSortedSet of S
  proof
    assume
A1: M is order-sorted;
    So1 is order-sorted
    proof
      let s1,s2;
      thus thesis by A1,Def17;
    end;
    hence thesis;
  end;
  assume
A2: So is OrderSortedSet of S;
  let s1,s2;
  thus thesis by A2,Def16;
end;

reserve CH for ManySortedFunction of ConstOSSet(S,z)# * the Arity of S,
  ConstOSSet(S,z) * the ResultSort of S;

definition
  let S,z,CH;
  func ConstOSA(S,z,CH) -> strict non-empty MSAlgebra over S means
  :Def18:
  the Sorts of it = ConstOSSet(S,z) & the Charact of it = CH;
  existence
  proof
    for i being set st i in the carrier of S holds ConstOSSet(S,z).i is
    non empty by FUNCOP_1:7;
    then ConstOSSet(S,z) is non-empty by PBOOLE:def 13;
    then reconsider T = MSAlgebra(# ConstOSSet(S,z),CH #) as strict non-empty
    MSAlgebra over S by MSUALG_1:def 3;
    take T;
    thus thesis;
  end;
  uniqueness;
end;

theorem Th18:
  ConstOSA(S,z,CH) is order-sorted
proof
  the Sorts of ConstOSA(S,z,CH) = ConstOSSet(S,z) by Def18;
  hence thesis by Th17;
end;

registration
  let S;
  cluster strict non-empty order-sorted for MSAlgebra over S;
  existence
  proof

set z = the non empty set,CH = the ManySortedFunction of ConstOSSet(S,z)# * the
Arity of S, ConstOSSet(S,z) * the ResultSort of S;
    take ConstOSA(S,z,CH);
    thus thesis by Th18;
  end;
end;

registration
  let S,z,CH;
  cluster ConstOSA(S,z,CH) -> order-sorted;
  coherence by Th18;
end;

definition
  let S;
  mode OSAlgebra of S is order-sorted MSAlgebra over S;
end;

theorem Th19:
  for S being discrete OrderSortedSign, M being MSAlgebra over S
  holds M is order-sorted
proof
  let S be discrete OrderSortedSign, M be MSAlgebra over S;
  let s1,s2 be SortSymbol of S;
  assume s1 <= s2;
  hence thesis by ORDERS_3:1;
end;

registration
  let S be discrete OrderSortedSign;
  cluster -> order-sorted for MSAlgebra over S;
  coherence by Th19;
end;

reserve A for OSAlgebra of S;

theorem Th20:
  w1 <= w2 implies (the Sorts of A)#.w1 c= (the Sorts of A)#.w2
proof
  set iw1 = (the Sorts of A) * w1, iw2 = (the Sorts of A) * w2;
  assume
A1: w1 <= w2;
  then
A2: len w1 = len w2 by Def6;
  let x be set;
  assume x in (the Sorts of A)#.w1;
  then x in product(iw1) by FINSEQ_2:def 5;
  then consider g being Function such that
A3: x = g and
A4: dom g = dom iw1 and
A5: for y being set st y in dom iw1 holds g.y in iw1.y by CARD_3:def 5;
A6: dom iw1 = dom w1 by Lm1
    .= dom w2 by A2,FINSEQ_3:29
    .= dom iw2 by Lm1;
  for y being set st y in dom iw2 holds g.y in iw2.y
  proof
    let y be set such that
A7: y in dom iw2;
A8: y in dom w1 by A6,A7,Lm1;
    then
A9: iw1.y = (the Sorts of A).(w1.y) by FUNCT_1:13;
A10: y in dom w2 by A7,Lm1;
    then
A11: iw2.y = (the Sorts of A).(w2.y) by FUNCT_1:13;
    reconsider s1 = w1.y, s2 = w2.y as SortSymbol of S by A8,A10,PARTFUN1:4;
    s1 <= s2 by A1,A8,Def6;
    then
A12: (the Sorts of A).(w1.y) c= (the Sorts of A).(w2.y) by Def17;
    g.y in iw1.y by A5,A6,A7;
    hence thesis by A9,A11,A12;
  end;
  then g in product(iw2) by A4,A6,CARD_3:def 5;
  hence thesis by A3,FINSEQ_2:def 5;
end;

reserve M for MSAlgebra over S0;

:: canonical OSAlgebra for MSAlgebra

definition
  let S0,M;
  func OSAlg M -> strict OSAlgebra of OSSign S0 means
  the Sorts of it = the Sorts of M & the Charact of it = the Charact of M;
  uniqueness;
  existence
  proof
    set S1 = OSSign S0, s0 = the Sorts of M, c0 = the Charact of M;
A1: the carrier of S0 = the carrier of S1 by Def5;
    then reconsider s1 = s0 as ManySortedSet of S1;
    the Arity of S0 = the Arity of S1 & the ResultSort of S1 = the
    ResultSort of S0 by Def5;
    then reconsider
    c1 = c0 as ManySortedFunction of s1# * the Arity of S1, s1 *
    the ResultSort of S1 by A1,Def5;
    MSAlgebra(# s1, c1 #) is order-sorted;
    hence thesis;
  end;
end;

:: monotone OSAlgebra

reserve A for OSAlgebra of S;

:: Element of A should mean Element of Union the Sorts of A here ...
:: MSAFREE3:def 1; Element of A,s is defined in MSUALG_6

theorem Th21:
  for w1,w2,w3 being Element of (the carrier of S)* holds w1 <= w2
  & w2 <= w3 implies w1 <= w3
proof
  let w1,w2,w3 be Element of (the carrier of S)*;
  assume that
A1: w1 <= w2 and
A2: w2 <= w3;
A3: len w1 = len w2 by A1,Def6;
  then
A4: dom w1 = dom w2 by FINSEQ_3:29;
A5: len w2 = len w3 by A2,Def6;
  then
A6: dom w2 = dom w3 by FINSEQ_3:29;
  for i being set st i in dom w1 for s1,s2 st s1 = w1.i & s2 = w3.i holds
  s1 <= s2
  proof
    let i be set such that
A7: i in dom w1;
    reconsider s3 = w1.i, s4 = w2.i, s5 = w3.i as SortSymbol of S by A4,A6,A7,
PARTFUN1:4;
A8: s3 <= s4 & s4 <= s5 by A1,A2,A4,A7,Def6;
    let s1,s2;
    assume s1 = w1.i & s2 = w3.i;
    hence thesis by A8,ORDERS_2:3;
  end;
  hence thesis by A3,A5,Def6;
end;

definition
  let S,o1,o2;
  pred o1 <= o2 means
  :Def20:
  o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2
  ) & the_result_sort_of o1 <= the_result_sort_of o2;
  reflexivity;
end;

theorem
  o1 <= o2 & o2 <= o1 implies o1 = o2
proof
  assume that
A1: o1 <= o2 and
A2: o2 <= o1;
  the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2
  <= the_result_sort_of o1 by A1,A2,Def20;
  then
A3: the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
  (the_arity_of o1) <= (the_arity_of o2) & (the_arity_of o2) <= (
  the_arity_of o1) by A1,A2,Def20;
  then
A4: the_arity_of o1 = the_arity_of o2 by Th6;
  o1 ~= o2 by A1,Def20;
  hence thesis by A4,A3,Def3;
end;

theorem
  o1 <= o2 & o2 <= o3 implies o1 <= o3
proof
  assume
A1: o1 <= o2 & o2 <= o3;
  then o1 ~= o2 & o2 ~= o3 by Def20;
  hence o1 ~= o3 by Th2;
  (the_arity_of o1) <= (the_arity_of o2) & (the_arity_of o2) <= (
  the_arity_of o3) by A1,Def20;
  hence (the_arity_of o1) <= (the_arity_of o3) by Th21;
  the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2
  <= the_result_sort_of o3 by A1,Def20;
  hence thesis by ORDERS_2:3;
end;

theorem Th24:
  the_result_sort_of o1 <= the_result_sort_of o2 implies Result(o1
  ,A) c= Result(o2,A)
proof
  reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: Result(o2,A) = ((the Sorts of A) * the ResultSort of S).o2 by
MSUALG_1:def 5
    .= (the Sorts of A).((the ResultSort of S).o2) by FUNCT_2:15
    .= (the Sorts of A).(the_result_sort_of o2) by MSUALG_1:def 2;
  assume the_result_sort_of o1 <= the_result_sort_of o2;
  then
A2: M.(the_result_sort_of o1) c= M.(the_result_sort_of o2) by Def16;
  Result(o1,A) = ((the Sorts of A) * the ResultSort of S).o1 by MSUALG_1:def 5
    .= (the Sorts of A).((the ResultSort of S).o1) by FUNCT_2:15
    .= (the Sorts of A).(the_result_sort_of o1) by MSUALG_1:def 2;
  hence thesis by A2,A1;
end;

theorem Th25:
  the_arity_of o1 <= the_arity_of o2 implies Args(o1,A) c= Args(o2 ,A)
proof
  reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: M#.(the_arity_of o1) = M#.((the Arity of S).o1) by MSUALG_1:def 1
    .= (M# * (the Arity of S)).o1 by FUNCT_2:15
    .= Args(o1,A) by MSUALG_1:def 4;
A2: M#.(the_arity_of o2) = M#.((the Arity of S).o2) by MSUALG_1:def 1
    .= (M# * (the Arity of S)).o2 by FUNCT_2:15
    .= Args(o2,A) by MSUALG_1:def 4;
  assume the_arity_of o1 <= the_arity_of o2;
  hence thesis by A1,A2,Th20;
end;

theorem
  o1 <= o2 implies Args(o1,A) c= Args(o2,A) & Result(o1,A) c= Result(o2, A )
proof
  assume o1 <= o2;
  then the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <=
  the_result_sort_of o2 by Def20;
  hence thesis by Th24,Th25;
end;

:: OSAlgebra is monotone iff the interpretation of the same symbol on
:: widening sorts coincides
:: the definition would be nicer as function inclusion (see TEqMon)
:: without the restriction to Args(o1,A), but the permissiveness
:: of FUNCT_2:def 1 spoils that

definition
  let S,A;
  attr A is monotone means
  :Def21:
  for o1,o2 st o1 <= o2 holds Den(o2,A)|Args( o1,A) = Den(o1,A);
end;

theorem Th27:
  for A being non-empty OSAlgebra of S holds A is monotone iff for
  o1,o2 st o1 <= o2 holds Den(o1,A) c= Den(o2,A)
proof
  let A be non-empty OSAlgebra of S;
  hereby
    assume
A1: A is monotone;
    let o1,o2;
    assume o1 <= o2;
    then Den(o2,A)|Args(o1,A) = Den(o1,A) by A1,Def21;
    hence Den(o1,A) c= Den(o2,A) by RELAT_1:59;
  end;
  assume
A2: for o1,o2 st o1 <= o2 holds Den(o1,A) c= Den(o2,A);
  let o1,o2 such that
A3: o1 <= o2;
 dom Den(o1,A) = Args(o1,A) by FUNCT_2:def 1;
  hence Den(o2,A)|Args(o1,A) = Den(o1,A)|Args(o1,A) by A2,A3,GRFUNC_1:27
    .= Den(o1,A);
end;

theorem
  (S is discrete or S is op-discrete) implies A is monotone
proof
  assume
A1: S is discrete or S is op-discrete;
  let o1,o2;
  assume that
A2: o1 ~= o2 and
A3: (the_arity_of o1) <= (the_arity_of o2) & the_result_sort_of o1 <=
  the_result_sort_of o2;
  o1 = o2
  proof
    per cases by A1;
    suppose
      S is discrete;
      hence thesis by A2,A3,Th8;
    end;
    suppose
      S is op-discrete;
      hence thesis by A2,Th3;
    end;
  end;
  hence thesis by RELSET_1:19;
end;

:: TrivialOSA(S,z,z1) interprets all funcs as one constant

definition
  let S,z;
  let z1 be Element of z;
  func TrivialOSA(S,z,z1) -> strict OSAlgebra of S means
  :Def22:
  the Sorts of
  it = ConstOSSet(S,z) & for o holds Den(o,it) = Args(o,it) --> z1;
  existence
  proof
    set c = ConstOSSet(S,z);
    deffunc ch1(Element of the carrier' of S) = ((c# * the Arity of S).$1) -->
    (z1 qua set);
    consider ch2 being Function such that
A1: dom ch2 = the carrier' of S & for x being Element of (the carrier'
    of S) holds ch2.x = ch1(x) from FUNCT_1:sch 4;
    reconsider ch4 = ch2 as ManySortedSet of (the carrier' of S) by A1,
PARTFUN1:def 2,RELAT_1:def 18;
    for i being set st i in (the carrier' of S) holds ch4.i is Function of
(ConstOSSet(S,z)# * the Arity of S).i, (ConstOSSet(S,z) * the ResultSort of S).
    i
    proof
      let i be set;
      assume i in the carrier' of S;
      then reconsider o=i as OperSymbol of S;
      (the ResultSort of S).o in the carrier of S;
      then
A2:   o in ((the ResultSort of S)"(the carrier of S)) by FUNCT_2:38;
      (ConstOSSet(S,z) * the ResultSort of S).o = (((the ResultSort of S)"
      (the carrier of S)) --> z).o by FUNCOP_1:19
        .= z by A2,FUNCOP_1:7;
      then
A3:   {z1} c= (ConstOSSet(S,z) * the ResultSort of S).i by ZFMISC_1:31;
      ch4.i = ch1(o) by A1;
      hence thesis by A3,FUNCT_2:7;
    end;
    then reconsider ch3 = ch4 as ManySortedFunction of (ConstOSSet(S,z)# * the
    Arity of S), (ConstOSSet(S,z) * the ResultSort of S) by PBOOLE:def 15;
    take T = ConstOSA(S,z,ch3);
    thus
A4: the Sorts of T = ConstOSSet(S,z) by Def18;
    let o;
    Den(o,T) = (the Charact of T).o by MSUALG_1:def 6
      .= ch3.o by Def18
      .= ((c# * the Arity of S).o) --> z1 by A1
      .= Args(o,T) --> z1 by A4,MSUALG_1:def 4;
    hence thesis;
  end;
  uniqueness
  proof
    let T1,T2 be strict OSAlgebra of S;
    assume that
A5: the Sorts of T1 = ConstOSSet(S,z) and
A6: for o holds Den(o,T1) = Args(o,T1) --> z1;
    assume that
A7: the Sorts of T2 = ConstOSSet(S,z) and
A8: for o holds Den(o,T2) = Args(o,T2) --> z1;
    now
      let o1 be set;
      assume o1 in the carrier' of S;
      then reconsider o = o1 as OperSymbol of S;
      thus (the Charact of T1).o1 = Den(o,T1) by MSUALG_1:def 6
        .= Args(o,T1) --> z1 by A6
        .= ((ConstOSSet(S,z)# * the Arity of S).o) --> z1 by A5,MSUALG_1:def 4
        .= Args(o,T2) --> z1 by A7,MSUALG_1:def 4
        .= Den(o,T2) by A8
        .= (the Charact of T2).o1 by MSUALG_1:def 6;
    end;
    hence thesis by A5,A7,PBOOLE:3;
  end;
end;

theorem Th29:
  for z1 being Element of z holds TrivialOSA(S,z,z1) is non-empty
  & TrivialOSA(S,z,z1) is monotone
proof
  let z1 be Element of z;
  set A = TrivialOSA(S,z,z1);
  the Sorts of A = ConstOSSet(S,z) by Def22;
  then
A1: the Sorts of A is non-empty by Th15;
  hence A is non-empty by MSUALG_1:def 3;
  reconsider A1 = A as non-empty OSAlgebra of S by A1,MSUALG_1:def 3;
  for o1,o2 st o1 <= o2 holds Den(o1,A1) c= Den(o2,A1)
  proof
    let o1,o2;
A2: Args(o1,A) = ((the Sorts of A)# * the Arity of S).o1 by MSUALG_1:def 4
      .= (the Sorts of A)#.((the Arity of S).o1) by FUNCT_2:15
      .= (the Sorts of A)#.(the_arity_of o1) by MSUALG_1:def 1;
A3: Args(o2,A) = ((the Sorts of A)# * the Arity of S).o2 by MSUALG_1:def 4
      .= (the Sorts of A)#.((the Arity of S).o2) by FUNCT_2:15
      .= (the Sorts of A)#.(the_arity_of o2) by MSUALG_1:def 1;
    assume o1 <= o2;
    then
A4: (the_arity_of o1) <= (the_arity_of o2) by Def20;
    Den(o1,A) = Args(o1,A) --> z1 & Den(o2,A) = Args(o2,A) --> z1 by Def22;
    hence thesis by A4,A2,A3,Th20,FUNCT_4:4;
  end;
  hence thesis by Th27;
end;

registration
  let S;
  cluster monotone strict non-empty for OSAlgebra of S;
  existence
  proof
    set z = the non empty set;
    set z1 = the Element of z;
    take TrivialOSA(S,z,z1);
    thus thesis by Th29;
  end;
end;

registration
  let S,z;
  let z1 be Element of z;
  cluster TrivialOSA(S,z,z1) -> monotone non-empty;
  coherence by Th29;
end;

:: OperNames, OperName, Name

reserve op1,op2 for OperSymbol of S;

definition
  let S;
  func OperNames S -> non empty (Subset-Family of the carrier' of S) equals
  Class the Overloading of S;
  coherence;
end;

registration
  let S;
  cluster -> non empty for Element of OperNames S;
  coherence
  proof
    let X be Element of OperNames S;
    ex x being set st x in the carrier' of S & X = Class(the Overloading of
    S,x) by EQREL_1:def 3;
    hence thesis by EQREL_1:20;
  end;
end;

definition
  let S;
  mode OperName of S is Element of OperNames S;
end;

definition
  let S,op1;
  func Name op1 -> OperName of S equals
  Class(the Overloading of S,op1);
  coherence by EQREL_1:def 3;
end;

theorem Th30:
  op1 ~= op2 iff op2 in Class(the Overloading of S,op1)
proof
  op1 ~= op2 iff [op2,op1] in the Overloading of S by Def2;
  hence thesis by EQREL_1:19;
end;

theorem Th31:
  op1 ~= op2 iff Name op1 = Name op2
proof
  op2 in Class(the Overloading of S,op1) iff Class(the Overloading of S,
  op1) = Class(the Overloading of S,op2) by EQREL_1:23;
  hence thesis by Th30;
end;

theorem
  for X being set holds X is OperName of S iff ex op1 st X = Name op1
proof
  let X be set;
  hereby
    assume X is OperName of S;
    then consider x being set such that
A1: x in the carrier' of S and
A2: X = Class(the Overloading of S,x) by EQREL_1:def 3;
    reconsider x1 = x as OperSymbol of S by A1;
    take x1;
    thus X = Name x1 by A2;
  end;
  given op1 such that
A3: X = Name op1;
  thus thesis by A3;
end;

definition
  let S;
  let o be OperName of S;
  redefine mode Element of o -> OperSymbol of S;
  coherence
  proof
    let x be Element of o;
    thus thesis;
  end;
end;

theorem Th33:
  for on being OperName of S, op being OperSymbol of S holds op is
  Element of on iff Name op = on
proof
  let on be OperName of S, op1 be OperSymbol of S;
  hereby
    assume op1 is Element of on;
    then reconsider op = op1 as Element of on;
    (ex op2 being set st op2 in the carrier' of S & on = Class (the
Overloading of S,op2) )& Name op = Class(the Overloading of S,op) by
EQREL_1:def 3;
    hence Name op1 = on by EQREL_1:23;
  end;
  assume Name op1 = on;
  hence thesis by EQREL_1:20;
end;

theorem Th34:
  for SR being regular monotone OrderSortedSign, op1,op2 being
OperSymbol of SR, w being Element of (the carrier of SR)* st op1 ~= op2 & w <=
  the_arity_of op1 & w <= the_arity_of op2 holds LBound(op1,w) = LBound(op2,w)
proof
  let SR be regular monotone OrderSortedSign, op1,op2 be OperSymbol of SR, w
  be Element of (the carrier of SR)* such that
A1: op1 ~= op2 and
A2: w <= the_arity_of op1 and
A3: w <= the_arity_of op2;
  set Lo1 = LBound(op1,w), Lo2 = LBound(op2,w);
A4: LBound(op1,w) has_least_args_for op1,w by A2,Def14;
  then
A5: op1 ~= Lo1 by Def9;
A6: LBound(op2,w) has_least_args_for op2,w by A3,Def14;
  then
A7: for o2 being OperSymbol of SR st op2 ~= o2 & w <= the_arity_of o2 holds
  the_arity_of Lo2 <= the_arity_of o2 by Def9;
  op2 ~= Lo2 by A6,Def9;
  then
A8: op1 ~= Lo2 by A1,Th2;
  then
A9: Lo1 ~= Lo2 by A5,Th2;
  w <= the_arity_of Lo1 by A4,Def9;
  then
A10: the_arity_of Lo2 <= the_arity_of Lo1 by A1,A5,A7,Th2;
  then
A11: the_result_sort_of Lo2 <= the_result_sort_of Lo1 by A9,Def7;
  w <= the_arity_of Lo2 by A6,Def9;
  then
A12: the_arity_of Lo1 <= the_arity_of Lo2 by A4,A8,Def9;
  then
A13: the_arity_of Lo1 = the_arity_of Lo2 by A10,Th6;
  the_result_sort_of Lo1 <= the_result_sort_of Lo2 by A9,A12,Def7;
  then the_result_sort_of Lo1 = the_result_sort_of Lo2 by A11,ORDERS_2:2;
  hence thesis by A9,A13,Def3;
end;

definition
  let SR be regular monotone OrderSortedSign, on be OperName of SR, w be
  Element of (the carrier of SR)*;
  assume
A1: ex op being Element of on st w <= the_arity_of op;
  func LBound(on,w) -> Element of on means
  for op being Element of on st w <= the_arity_of op holds it = LBound(op,w);
  existence
  proof
    consider op being Element of on such that
A2: w <= the_arity_of op by A1;
    set Lo = LBound(op,w);
    LBound(op,w) has_least_args_for op,w by A2,Def14;
    then op ~= Lo by Def9;
    then
A3: Name(op) = Name Lo by Th31;
    then
A4: Name Lo = on by Th33;
    then reconsider Lo as Element of on by Th33;
    take Lo;
    let op1 be Element of on such that
A5: w <= the_arity_of op1;
    Name op1 = on by Th33;
    then op1 ~= op by A3,A4,Th31;
    hence thesis by A2,A5,Th34;
  end;
  uniqueness
  proof
    let op1,op2 be Element of on such that
A6: for op3 being Element of on st w <= the_arity_of op3 holds op1 =
    LBound(op3,w) and
A7: for op3 being Element of on st w <= the_arity_of op3 holds op2 =
    LBound(op3,w);
    consider op being Element of on such that
A8: w <= the_arity_of op by A1;
    op1 = LBound(op,w) by A8,A6;
    hence thesis by A8,A7;
  end;
end;

theorem
  for S being regular monotone OrderSortedSign, o being OperSymbol of
S, w1 being Element of (the carrier of S)* st w1 <= the_arity_of o holds LBound
  (o,w1) <= o
proof
  let S being regular monotone OrderSortedSign, o being OperSymbol of S, w1
  being Element of (the carrier of S)* such that
A1: w1 <= the_arity_of o;
  set lo = LBound(o,w1);
A2: lo has_least_rank_for o,w1 by A1,Th14;
  then lo has_least_sort_for o,w1 by Def11;
  then
A3: the_result_sort_of lo <= the_result_sort_of o by A1,Def10;
A4: lo has_least_args_for o,w1 by A2,Def11;
  then
A5: o ~= lo by Def9;
  the_arity_of lo <= the_arity_of o by A1,A4,Def9;
  hence thesis by A5,A3,Def20;
end;