PBOOLE

:: Manysorted Sets
::  by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1,
      FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1,
      SETLIM_2;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1;
 constructors SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4,
      RELAT_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1;
 equalities XBOOLE_0;
 expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
 theorems TARSKI, FUNCOP_1, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1, FUNCT_2,
      PARTFUN1, FUNCT_4, ZFMISC_1, SETFAM_1;
 schemes FUNCT_1, CLASSES1, XBOOLE_0;

begin

reserve i,j,e,u for object;

theorem
  for f being Function st f is non-empty holds rng f is
  with_non-empty_elements;

theorem
  for f being Function holds f is empty-yielding iff f = {} or rng f = {
  {} }
proof
  let f be Function;
  hereby
    assume that
A1: f is empty-yielding and
A2: f <> {};
    thus rng f = { {} }
    proof
      thus for i being object st i in rng f holds i in { {} }
      by A1;
      set e = the Element of dom f;
      let i be object;
      assume i in { {} };
      then
A3:   i = {} by TARSKI:def 1;
A4:   dom f <> {} by A2;
      f.e is empty by A1;
      hence thesis by A4,A3,FUNCT_1:def 3;
    end;
  end;
  assume
A5: f = {} or rng f = { {} };
  per cases by A5;
  suppose
    f = {};
    hence for i being object st i in dom f holds f.i is empty;
  end;
  suppose
A6: rng f = { {} };
    let i be object;
    assume i in dom f;
    then f.i in rng f by FUNCT_1:def 3;
    hence thesis by A6,TARSKI:def 1;
  end;
end;

reserve I for set; :: of indices

registration
  let I;
  cluster total for I-defined Function;
  existence
  proof
    take I --> {};
    thus thesis;
  end;
end;

definition
  let I;
  mode ManySortedSet of I is total I-defined Function;
end;

reserve x,X,Y,Z,V for ManySortedSet of I;

scheme
  KuratowskiFunction{A()-> set, F(object) -> set}:
 ex f being ManySortedSet of A() st
  for e being object st e in A() holds f.e in F(e)
provided
A1: for e being object st e in A() holds F(e) <> {}
proof
  defpred P[object,object] means $2 in F($1);
A2: now
    let e be object;
    set fe = the Element of F(e);
    assume
A3: e in A();
    reconsider fe as object;
    take fe;
    F(e) <> {} by A1,A3;
    hence P[e,fe];
  end;
  consider f being Function such that
A4: dom f = A() and
A5: for e being object st e in A() holds P[e,f.e] from CLASSES1:sch 1(A2);
  reconsider f as ManySortedSet of A() by A4,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A5;
end;

definition
  let I,X,Y;
  pred X in Y means

  for i being object st i in I holds X.i in Y.i;
  pred X c= Y means

  for i being object st i in I holds X.i c= Y.i;
  reflexivity;
end;

definition
  let I be non empty set,X,Y be ManySortedSet of I;
  redefine pred X in Y;  :: redefines in (PBOOLE, definition)
  asymmetry
  proof
    let X,Y be ManySortedSet of I;
    assume
A1: for i being object st i in I holds X.i in Y.i;
    not for i st i in I holds Y.i in X.i
    proof
      assume
A2:   for i st i in I holds Y.i in X.i;
      consider i being object such that
A3:   i in I by XBOOLE_0:def 1;
      X.i in Y.i by A1,A3;
      hence thesis by A2,A3;
    end;
    hence thesis;
  end;
end;

scheme
  PSeparation { I()-> set, A() -> ManySortedSet of I(), P[object,object] } :
   ex X being ManySortedSet of I() st
    for i being object st i in I()
     for e being object holds e in X.i iff e in A().i & P[i,e];
  defpred R[object,object] means
   ex A being set st A = $2 &
   for e being object holds e in A iff e in A().$1 & P[ $1,e];
A1: now
    let i be object such that
    i in I();
    defpred Q[object] means P[i,$1];
    ex u being set
     st for e being object holds e in u iff e in A().i & Q[e]
    from XBOOLE_0:sch 1;
    hence ex u being object st R[i,u];
  end;
  consider f being Function such that
A2: dom f = I() and
A3: for i being object st i in I() holds R[i,f.i] from CLASSES1:sch 1(A1);
  reconsider f as ManySortedSet of I() by A2,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  let i be object;
  assume i in I();
   then R[i,f.i] by A3;
  hence thesis;
end;

theorem Th3:
  (for i being object st i in I holds X.i = Y.i) implies X = Y
proof
  dom X = I & dom Y = I by PARTFUN1:def 2;
  hence thesis;
end;

definition
  let I;
  func EmptyMS I -> ManySortedSet of I equals
  I --> {};
  coherence;
  correctness;
  let X,Y;
  func X (\/) Y -> ManySortedSet of I means
  :Def4:
  for i being object st i in I holds it.i = X.i \/ Y.i;
  existence
  proof
    deffunc F(object) = X.$1 \/ Y.$1;
    consider f being Function such that
A1: dom f = I and
A2: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
    f is ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let A1, A2 be ManySortedSet of I such that
A3: for i being object st i in I holds A1.i = X.i \/ Y.i and
A4: for i being object st i in I holds A2.i = X.i \/ Y.i;
    now
      let i be object;
      assume
A5:   i in I;
      hence A1.i = X.i \/ Y.i by A3
        .= A2.i by A4,A5;
    end;
    hence thesis by Th3;
  end;
  commutativity;
  idempotence;
  func X (/\) Y -> ManySortedSet of I means
  :Def5:
  for i being object st i in I holds it.i = X.i /\ Y.i;
  existence
  proof
    deffunc F(object) = X.$1 /\ Y.$1;
    consider f being Function such that
A6: dom f = I and
A7: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
    f is ManySortedSet of I by A6,PARTFUN1:def 2,RELAT_1:def 18;
    hence thesis by A7;
  end;
  uniqueness
  proof
    let A1, A2 be ManySortedSet of I such that
A8: for i being object st i in I holds A1.i = X.i /\ Y.i and
A9: for i being object st i in I holds A2.i = X.i /\ Y.i;
    now
      let i be object;
      assume
A10:  i in I;
      hence A1.i = X.i /\ Y.i by A8
        .= A2.i by A9,A10;
    end;
    hence thesis by Th3;
  end;
  commutativity;
  idempotence;
  func X (\) Y -> ManySortedSet of I means
  :Def6:
  for i being object st i in I holds it.i = X.i \ Y.i;
  existence
  proof
    deffunc F(object) = X.$1 \ Y.$1;
    consider f being Function such that
A11: dom f = I and
A12: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
    f is ManySortedSet of I by A11,PARTFUN1:def 2,RELAT_1:def 18;
    hence thesis by A12;
  end;
  uniqueness
  proof
    let A1, A2 be ManySortedSet of I such that
A13: for i being object st i in I holds A1.i = X.i \ Y.i and
A14: for i being object st i in I holds A2.i = X.i \ Y.i;
    now
      let i be object;
      assume
A15:  i in I;
      hence A1.i = X.i \ Y.i by A13
        .= A2.i by A14,A15;
    end;
    hence thesis by Th3;
  end;
  pred X overlaps Y means

  for i being object st i in I holds X.i meets Y.i;
  symmetry;
  pred X misses Y means

  for i being object st i in I holds X.i misses Y.i;
  symmetry;
end;

notation
  let I;
  let X,Y;
  antonym X meets Y for X misses Y;
end;

definition
  let I,X,Y;
  func X (\+\) Y -> ManySortedSet of I equals
  (X (\) Y) (\/) (Y (\) X);
  correctness;
  commutativity;
end;

theorem Th4:
  for i st i in I holds (X (\+\) Y).i = X.i \+\ Y.i
proof
  let i such that
A1: i in I;
  thus (X (\+\) Y).i = (X (\) Y).i \/ (Y (\) X).i by A1,Def4
    .= X.i \ Y.i \/ (Y (\) X).i by A1,Def6
    .= X.i \+\ Y.i by A1,Def6;
end;

theorem
  for i being object holds EmptyMS I.i = {};

theorem Th6:
  (for i being object st i in I holds X.i = {}) implies X = EmptyMS I
proof
  assume
A1: for i being object st i in I holds X.i = {};
  now
    let i be object;
    assume i in I;
    hence X.i = {} by A1
      .= EmptyMS I.i;
  end;
  hence thesis by Th3;
end;

theorem Th7:
  x in X or x in Y implies x in X (\/) Y
proof
  assume
A1: x in X or x in Y;
  let i be object;
  assume
A2: i in I;
  then x.i in X.i or x.i in Y.i by A1;
  then x.i in X.i \/ Y.i by XBOOLE_0:def 3;
  hence thesis by A2,Def4;
end;

theorem Th8:
  x in X (/\) Y iff x in X & x in Y
proof
  hereby
    assume
A1: x in X (/\) Y;
    thus x in X
    proof
      let i be object;
      assume
A2:   i in I;
      then x.i in (X (/\) Y).i by A1;
      then x.i in X.i /\ Y.i by A2,Def5;
      hence thesis by XBOOLE_0:def 4;
    end;
    thus x in Y
    proof
      let i be object;
      assume
A3:   i in I;
      then x.i in (X (/\) Y).i by A1;
      then x.i in X.i /\ Y.i by A3,Def5;
      hence thesis by XBOOLE_0:def 4;
    end;
  end;
  assume
A4: x in X & x in Y;
  let i be object;
  assume
A5: i in I;
  then x.i in X.i & x.i in Y.i by A4;
  then x.i in X.i /\ Y.i by XBOOLE_0:def 4;
  hence thesis by A5,Def5;
end;

theorem Th9:
  x in X & X c= Y implies x in Y
proof
  assume
A1: x in X & X c= Y;
  let i be object;
  assume i in I;
  then x.i in X.i & X.i c= Y.i by A1;
  hence thesis;
end;

theorem Th10:
  x in X & x in Y implies X overlaps Y
proof
  assume
A1: x in X & x in Y;
  let i be object;
  assume i in I;
  then x.i in X.i & x.i in Y.i by A1;
  hence thesis by XBOOLE_0:3;
end;

theorem Th11:
  X overlaps Y implies ex x st x in X & x in Y
proof
  deffunc F(object) = X.$1 /\ Y.$1;
  assume
A1: X overlaps Y;
A2: for i being object st i in I holds F(i) <> {} by XBOOLE_0:def 7,A1;
  consider x being ManySortedSet of I such that
A3: for i being object st i in I holds x.i in F(i)
   from KuratowskiFunction(A2);
  take x;
  now
    let i be object;
    assume i in I;
    then x.i in X.i /\ Y.i by A3;
    hence x.i in X.i by XBOOLE_0:def 4;
  end;
  hence x in X;
  now
    let i be object;
    assume i in I;
    then x.i in X.i /\ Y.i by A3;
    hence x.i in Y.i by XBOOLE_0:def 4;
  end;
  hence thesis;
end;

theorem
  x in X (\) Y implies x in X
proof
  assume
A1: x in X (\) Y;
  thus x in X
  proof
    let i be object;
    assume
A2: i in I;
    then x.i in (X (\) Y).i by A1;
    then x.i in X.i \ Y.i by A2,Def6;
    hence thesis;
  end;
end;

begin :: Lattice properties

Lm1:
 X c= Y & Y c= X implies X = Y
  proof
    assume X c= Y & Y c= X;
    then for i be object st i in I holds X.i = Y.i;
    hence thesis by Th3;
  end;

definition
  let I,X,Y;
  redefine pred X = Y means  :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  for i being object st i in I holds X.i = Y.i;
  compatibility by Th3;
end;

theorem Th13:
  X c= Y & Y c= Z implies X c= Z
proof
  assume that
A1: X c= Y and
A2: Y c= Z;
  let i be object such that
A3: i in I;
  let e be object;
  assume
A4: e in X.i;
  X.i c= Y.i by A1,A3;
  then
A5: e in Y.i by A4;
  Y.i c= Z.i by A2,A3;
  hence thesis by A5;
end;

theorem Th14:
  X c= X (\/) Y
proof
    let i be object such that
A1: i in I;
    let e be object;
    assume e in X.i;
    then e in X.i \/ Y.i by XBOOLE_0:def 3;
    hence thesis by A1,Def4;
end;

theorem Th15:
  X (/\) Y c= X
proof
    let i be object such that
A1: i in I;
    let e be object;
    assume e in (X (/\) Y).i;
    then e in X.i /\ Y.i by A1,Def5;
    hence thesis by XBOOLE_0:def 4;
end;

theorem Th16:
  X c= Z & Y c= Z implies X (\/) Y c= Z
proof
  assume
A1: X c= Z & Y c= Z;
  let i be object;
  assume
A2: i in I;
  then X.i c= Z.i & Y.i c= Z.i by A1;
  then X.i \/ Y.i c= Z.i by XBOOLE_1:8;
  hence thesis by A2,Def4;
end;

theorem Th17:
  Z c= X & Z c= Y implies Z c= X (/\) Y
proof
  assume
A1: Z c= X & Z c= Y;
  let i be object;
  assume
A2: i in I;
  then Z.i c= X.i & Z.i c= Y.i by A1;
  then Z.i c= X.i /\ Y.i by XBOOLE_1:19;
  hence thesis by A2,Def5;
end;

theorem
  X c= Y implies X (\/) Z c= Y (\/) Z
proof
  assume
A1: X c= Y;
A2: Z c= Y (\/) Z by Th14;
  Y c= Y (\/) Z by Th14;
  then X c= Y (\/) Z by A1,Th13;
  hence X (\/) Z c= Y (\/) Z by A2,Th16;
end;

theorem Th19:
  X c= Y implies X (/\) Z c= Y (/\) Z
proof
  assume
A1: X c= Y;
A2: X (/\) Z c= Z by Th15;
  X (/\) Z c= X by Th15;
  then X (/\) Z c= Y by A1,Th13;
  hence X (/\) Z c= Y (/\) Z by A2,Th17;
end;

theorem Th20:
  X c= Y & Z c= V implies X (\/) Z c= Y (\/) V
proof
  assume that
A1: X c= Y and
A2: Z c= V;
  V c= Y (\/) V by Th14;
  then
A3: Z c= Y (\/) V by A2,Th13;
  Y c= Y (\/) V by Th14;
  then X c= Y (\/) V by A1,Th13;
  hence thesis by A3,Th16;
end;

theorem
  X c= Y & Z c= V implies X (/\) Z c= Y (/\) V
proof
  assume that
A1: X c= Y and
A2: Z c= V;
  X (/\) Z c= Z by Th15;
  then
A3: X (/\) Z c= V by A2,Th13;
  X (/\) Z c= X by Th15;
  then X (/\) Z c= Y by A1,Th13;
  hence thesis by A3,Th17;
end;

theorem Th22:
  X c= Y implies X (\/) Y = Y
proof
  assume X c= Y;
  then
A1: X (\/) Y c= Y by Th16;
  Y c= X (\/) Y by Th14;
 hence thesis by A1,Lm1;
end;

theorem Th23:
  X c= Y implies X (/\) Y = X
proof
  assume
A1: X c= Y;
A2: X (/\) Y c= X by Th15;
  X c= X (/\) Y by A1,Th17;
 hence thesis by A2,Lm1;
end;

theorem
  X (/\) Y c= X (\/) Z
proof
  X (/\) Y c= X & X c= X (\/) Z by Th14,Th15;
  hence thesis by Th13;
end;

theorem
  X c= Z implies X (\/) Y (/\) Z = (X (\/) Y) (/\) Z
proof
  assume
A1: X c= Z;
    let i be object;
    assume
A2: i in I;
    then
A3: X.i c= Z.i by A1;
    thus (X (\/) Y (/\) Z).i = X.i \/ (Y (/\) Z).i by A2,Def4
      .= X.i \/ Y.i /\ Z.i by A2,Def5
      .= (X.i \/ Y.i) /\ Z.i by A3,XBOOLE_1:30
      .= (X (\/) Y).i /\ Z.i by A2,Def4
      .= ((X (\/) Y) (/\) Z).i by A2,Def5;
end;

theorem
  X = Y (\/) Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
proof
  thus X = Y (\/) Z implies Y c= X & Z c= X & for V st Y c= V & Z c= V holds X
  c= V by Th14,Th16;
  assume that
A1: Y c= X & Z c= X and
A2: Y c= V & Z c= V implies X c= V;
  Y c= Y (\/) Z & Z c= Y (\/) Z by Th14;
  then
A3: X c= Y (\/) Z by A2;
   Y (\/) Z c= X by A1,Th16;
 hence thesis by A3,Lm1;
end;

theorem
  X = Y (/\) Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X
proof
  thus X = Y (/\) Z implies X c= Y & X c= Z & for V st V c= Y & V c= Z holds V
  c= X by Th15,Th17;
  assume that
A1: X c= Y & X c= Z and
A2: V c= Y & V c= Z implies V c= X;
A3:  X c= Y (/\) Z by A1,Th17;
  Y (/\) Z c= Y & Y (/\) Z c= Z implies Y (/\) Z c= X by A2;
  hence thesis by A3,Lm1,Th15;
end;

theorem Th28:
  (X (\/) Y) (\/) Z = X (\/) (Y (\/) Z)
proof
    let i be object;
    assume
A1: i in I;
    hence (X (\/) Y (\/) Z).i = (X (\/) Y).i \/ Z.i by Def4
      .= X.i \/ Y.i \/ Z.i by A1,Def4
      .= X.i \/ (Y.i \/ Z.i) by XBOOLE_1:4
      .= X.i \/ (Y (\/) Z).i by A1,Def4
      .= (X (\/) (Y (\/) Z)).i by A1,Def4;
end;

theorem Th29:
  (X (/\) Y) (/\) Z = X (/\) (Y (/\) Z)
proof
    let i be object;
    assume
A1: i in I;
    hence (X (/\) Y (/\) Z).i = (X (/\) Y).i /\ Z.i by Def5
      .= X.i /\ Y.i /\ Z.i by A1,Def5
      .= X.i /\ (Y.i /\ Z.i) by XBOOLE_1:16
      .= X.i /\ (Y (/\) Z).i by A1,Def5
      .= (X (/\) (Y (/\) Z)).i by A1,Def5;
end;

theorem Th30:
  X (/\) (X (\/) Y) = X
proof
  X c= X (\/) Y by Th14;
  then
A1: X c= X (/\) (X (\/) Y) by Th17;
 X (/\) (X (\/) Y) c= X by Th15;
  hence X (/\) (X (\/) Y) = X by A1,Lm1;
end;

theorem Th31:
  X (\/) (X (/\) Y) = X
proof
  X (/\) Y c= X by Th15;
  then
A1: X (\/) (X (/\) Y) c= X by Th16;
 X c= X (\/) (X (/\) Y) by Th14;
  hence X (\/) (X (/\) Y) = X by A1,Lm1;
end;

theorem Th32:
  X (/\) (Y (\/) Z) = X (/\) Y (\/) X (/\) Z
proof
    let i be object;
    assume
A1: i in I;
    hence (X (/\) (Y (\/) Z)).i = X.i /\ (Y (\/) Z).i by Def5
      .= X.i /\ (Y.i \/ Z.i) by A1,Def4
      .= X.i /\ Y.i \/ X.i /\ Z.i by XBOOLE_1:23
      .= (X (/\) Y).i \/ X.i /\ Z.i by A1,Def5
      .= (X (/\) Y).i \/ (X (/\) Z).i by A1,Def5
      .= (X (/\) Y (\/) X (/\) Z).i by A1,Def4;
end;

theorem Th33:
  X (\/) Y (/\) Z = (X (\/) Y) (/\) (X (\/) Z)
proof
  thus X (\/) Y (/\) Z = X (\/) X (/\) Z (\/) Y (/\) Z by Th31
    .= X (\/) (X (/\) Z (\/) Y (/\) Z) by Th28
    .= X (\/) (X (\/) Y) (/\) Z by Th32
    .= (X (\/) Y) (/\) X (\/) (X (\/) Y) (/\) Z by Th30
    .= (X (\/) Y) (/\) (X (\/) Z) by Th32;
end;

theorem
  (X (/\) Y) (\/) (X (/\) Z) = X implies X c= Y (\/) Z
proof
  assume (X (/\) Y) (\/) (X (/\) Z) = X;
  then X = X (/\) (Y (\/) Z) by Th32;
  hence thesis by Th15;
end;

theorem
  (X (\/) Y) (/\) (X (\/) Z) = X implies Y (/\) Z c= X
proof
  assume (X (\/) Y) (/\) (X (\/) Z) = X;
  then X = X (\/) (Y (/\) Z) by Th33;
  hence thesis by Th14;
end;

theorem
  (X (/\) Y) (\/) (Y (/\) Z) (\/) (Z (/\) X)
    = (X (\/) Y) (/\) (Y (\/) Z) (/\) (Z (\/) X)
proof
  thus X (/\) Y (\/) Y (/\) Z (\/) Z (/\) X
      = (X (/\) Y (\/) Y (/\) Z (\/) Z) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X)
         by Th33
    .= (X (/\) Y (\/) (Y (/\) Z (\/) Z)) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X)
         by Th28
    .= (X (/\) Y (\/) Z) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X) by Th31
    .= (X (/\) Y (\/) Z) (/\) (X (/\) Y (\/) X (\/) Y (/\) Z) by Th28
    .= (X (/\) Y (\/) Z) (/\) (X (\/) Y (/\) Z) by Th31
    .= (X (\/) Z) (/\) (Y (\/) Z) (/\) (X (\/) Y (/\) Z) by Th33
    .= (X (\/) Z) (/\) (Y (\/) Z) (/\) ((X (\/) Y) (/\) (X (\/) Z)) by Th33
    .= (X (\/) Y) (/\) ((Y (\/) Z) (/\) (X (\/) Z) (/\) (X (\/) Z)) by Th29
    .= (X (\/) Y) (/\) ((Y (\/) Z) (/\) ((X (\/) Z) (/\) (X (\/) Z))) by Th29
    .= (X (\/) Y) (/\) (Y (\/) Z) (/\) (Z (\/) X) by Th29;
end;

theorem
  X (\/) Y c= Z implies X c= Z
proof
  X c= X (\/) Y by Th14;
  hence thesis by Th13;
end;

theorem
  X c= Y (/\) Z implies X c= Y
proof
  Y (/\) Z c= Y by Th15;
  hence thesis by Th13;
end;

theorem
  X (\/) Y (\/) Z = (X (\/) Z) (\/) (Y (\/) Z)
proof
  thus X (\/) Y (\/) Z = X (\/) (Y (\/) (Z (\/) Z)) by Th28
    .= X (\/) (Z (\/) Y (\/) Z) by Th28
    .= (X (\/) Z) (\/) (Y (\/) Z) by Th28;
end;

theorem
  X (/\) Y (/\) Z = (X (/\) Z) (/\) (Y (/\) Z)
proof
  thus X (/\) Y (/\) Z = X (/\) (Y (/\) (Z (/\) Z)) by Th29
    .= X (/\) (Z (/\) Y (/\) Z) by Th29
    .= (X (/\) Z) (/\) (Y (/\) Z) by Th29;
end;

theorem
  X (\/) (X (\/) Y) = X (\/) Y
proof
  thus X (\/) (X (\/) Y) = X (\/) X (\/) Y by Th28
    .= X (\/) Y;
end;

theorem
  X (/\) (X (/\) Y) = X (/\) Y
proof
  thus X (/\) (X (/\) Y) = X (/\) X (/\) Y by Th29
    .= X (/\) Y;
end;

begin :: ManySortedSet with empty components

theorem Th43:
  EmptyMS I c= X
proof
  let i be object such that
 i in I;
  let e be object;
  assume e in EmptyMS I.i;
  hence thesis;
end;

theorem Th44:
  X c= EmptyMS I implies X = EmptyMS I
proof
  assume X c= EmptyMS I;
   then X c= EmptyMS I & EmptyMS I c= X by Th43;
  hence thesis by Lm1;
end;

theorem
  X c= Y & X c= Z & Y (/\) Z = EmptyMS I implies X = EmptyMS I by Th17,Th44;

theorem
  X c= Y & Y (/\) Z = EmptyMS I implies X (/\) Z = EmptyMS I by Th44,Th19;

theorem
  X (\/) EmptyMS I = X & EmptyMS I (\/) X = X by Th22,Th43;

theorem
  X (\/) Y = EmptyMS I implies X = EmptyMS I by Th44,Th14;

theorem
  X (/\) EmptyMS I = EmptyMS I by Th23,Th43;

theorem
  X c= (Y (\/) Z) & X (/\) Z = EmptyMS I implies X c= Y
proof
  assume that
A1: X c= (Y (\/) Z) and
A2: X (/\) Z = EmptyMS I;
  X (/\) (Y (\/) Z)= X by A1,Th23;
  then Y (/\) X (\/) EmptyMS I = X by A2,Th32;
  then Y (/\) X = X by Th22,Th43;
  hence thesis by Th15;
end;

theorem
  Y c= X & X (/\) Y = EmptyMS I implies Y = EmptyMS I by Th23;

begin :: Difference and symmetric difference

theorem Th52:
  X (\) Y = EmptyMS I iff X c= Y
proof
  hereby
    assume
A1: X (\) Y = EmptyMS I;
    now
      let i be object;
      assume i in I;
      then X.i \ Y.i = (X (\) Y).i by Def6
        .= {} by A1;
      hence X.i c= Y.i by XBOOLE_1:37;
    end;
    hence X c= Y;
  end;
  assume
A2: X c= Y;
  now
    let i be object;
    assume
A3: i in I;
    then
A4: X.i c= Y.i by A2;
    thus (X (\) Y).i = X.i \ Y.i by A3,Def6
      .= {} by A4,XBOOLE_1:37;
  end;
  hence thesis by Th6;
end;

theorem Th53:
  X c= Y implies X (\) Z c= Y (\) Z
proof
  assume
A1: X c= Y;
  now
    let i be object;
    assume
A2: i in I;
    then
A3: (X (\) Z).i = X.i \ Z.i & (Y (\) Z).i = Y.i \ Z.i by Def6;
    X.i c= Y.i by A1,A2;
    hence (X (\) Z).i c= (Y (\) Z).i by A3,XBOOLE_1:33;
  end;
  hence thesis;
end;

theorem Th54:
  X c= Y implies Z (\) Y c= Z (\) X
proof
  assume
A1: X c= Y;
  now
    let i be object;
    assume
A2: i in I;
    then
A3: (Z (\) X).i = Z.i \ X.i & (Z (\) Y).i = Z.i \ Y.i by Def6;
    X.i c= Y.i by A1,A2;
    hence (Z (\) Y).i c= (Z (\) X).i by A3,XBOOLE_1:34;
  end;
  hence thesis;
end;

theorem
  X c= Y & Z c= V implies X (\) V c= Y (\) Z
proof
  assume X c= Y & Z c= V;
  then X (\) V c= Y (\) V & Y (\) V c= Y (\) Z by Th53,Th54;
  hence thesis by Th13;
end;

theorem Th56:
  X (\) Y c= X
proof
  now
    let i be object such that
A1: i in I;
    X.i \ Y.i c= X.i;
    hence (X (\) Y).i c= X.i by A1,Def6;
  end;
  hence thesis;
end;

theorem
  X c= Y (\) X implies X = EmptyMS I
proof
  assume
A1: X c= Y (\) X;
    let i be object;
    assume
A2: i in I;
    then X.i c= (Y (\) X).i by A1;
    then X.i c= Y.i \ X.i by A2,Def6;
    hence X.i = {} by XBOOLE_1:38
      .= EmptyMS I.i;
end;

theorem
  X (\) X = EmptyMS I by Th52;

theorem Th59:
  X (\) EmptyMS I = X
proof
    let i be object;
    assume i in I;
    hence (X (\) EmptyMS I).i = X.i \ EmptyMS I.i by Def6
      .= X.i \ {}
      .= X.i;
end;

theorem Th60:
  EmptyMS I (\) X = EmptyMS I
by Th43,Th52;

theorem
  X (\) (X (\/) Y) = EmptyMS I
by Th14,Th52;

theorem Th62:
  X (/\) (Y (\) Z) = (X (/\) Y) (\) Z
proof
    let i be object;
    assume
A1: i in I;
    hence (X (/\) (Y (\) Z)).i = X.i /\ (Y (\) Z).i by Def5
      .= X.i /\ (Y.i \ Z.i) by A1,Def6
      .= X.i /\ Y.i \ Z.i by XBOOLE_1:49
      .= (X (/\) Y).i \ Z.i by A1,Def5
      .= ((X (/\) Y) (\) Z).i by A1,Def6;
end;

theorem Th63:
  (X (\) Y) (/\) Y = EmptyMS I
proof
A1: Y (/\) X c= Y by Th15;
  thus (X (\) Y) (/\) Y = (Y (/\) X) (\) Y by Th62
    .= EmptyMS I by A1,Th52;
  thus thesis;
end;

theorem Th64:
  X (\) (Y (\) Z) = (X (\) Y) (\/) X (/\) Z
proof
    let i be object;
    assume
A1: i in I;
    hence (X (\) (Y (\) Z)).i = X.i \ (Y (\) Z).i by Def6
      .= X.i \ (Y.i \ Z.i) by A1,Def6
      .= X.i \ Y.i \/ X.i /\ Z.i by XBOOLE_1:52
      .= X.i \ Y.i \/ (X (/\) Z).i by A1,Def5
      .= (X (\) Y).i \/ (X (/\) Z).i by A1,Def6
      .= ((X (\) Y) (\/) X (/\) Z).i by A1,Def4;
end;

theorem Th65:
  (X (\) Y) (\/) X (/\) Y = X
proof
  thus X (\) Y (\/) X (/\) Y = X (\) (Y (\) Y) by Th64
    .= X (\) EmptyMS I by Th52
    .= X by Th59;
end;

theorem
  X c= Y implies Y = X (\/) (Y (\) X)
proof
  assume
A1: X c= Y;
  thus Y = (Y (\) X) (\/) Y (/\) X by Th65
    .= X (\/) (Y (\) X) by A1,Th23;
end;

theorem Th67:
  X (\/) (Y (\) X) = X (\/) Y
proof
  thus X (\/) (Y (\) X) = X (\/) Y (/\) X (\/) (Y (\) X) by Th31
    .= X (\/) (Y (/\) X (\/) (Y (\) X)) by Th28
    .= X (\/) Y by Th65;
end;

theorem Th68:
  X (\) (X (\) Y) = X (/\) Y
proof
  thus X (\) (X (\) Y) = (X (\) X) (\/) X (/\) Y by Th64
    .= EmptyMS I (\/) X (/\) Y by Th52
    .= X (/\) Y by Th22,Th43;
end;

theorem Th69:
  X (\) (Y (/\) Z) = (X (\) Y) (\/) (X (\) Z)
proof
    let i be object;
    assume
A1: i in I;
    hence (X (\) (Y (/\) Z)).i = X.i \ (Y (/\) Z).i by Def6
      .= X.i \ Y.i /\ Z.i by A1,Def5
      .= X.i \ Y.i \/ (X.i \ Z.i) by XBOOLE_1:54
      .= X.i \ Y.i \/ (X (\) Z).i by A1,Def6
      .= (X (\) Y).i \/ (X (\) Z).i by A1,Def6
      .= ((X (\) Y) (\/) (X (\) Z)).i by A1,Def4;
end;

theorem Th70:
  X (\) X (/\) Y = X (\) Y
proof
  thus X (\) X (/\) Y = (X (\) X) (\/) (X (\) Y) by Th69
    .= EmptyMS I (\/) (X (\) Y) by Th52
    .= X (\) Y by Th22,Th43;
end;

theorem
  X (/\) Y = EmptyMS I iff X (\) Y = X
proof
  hereby
    assume
A1: X (/\) Y = EmptyMS I;
    thus X (\) Y = X (\) X (/\) Y by Th70
      .= X by A1,Th59;
  end;
  thus thesis by Th63;
end;

theorem Th72:
  (X (\/) Y) (\) Z = (X (\) Z) (\/) (Y (\) Z)
proof
    let i be object;
    assume
A1: i in I;
    hence ((X (\/) Y) (\) Z).i = (X (\/) Y).i \ Z.i by Def6
      .= X.i \/ Y.i \ Z.i by A1,Def4
      .= X.i \ Z.i \/ (Y.i \ Z.i) by XBOOLE_1:42
      .= X.i \ Z.i \/ (Y (\) Z).i by A1,Def6
      .= (X (\) Z).i \/ (Y (\) Z).i by A1,Def6
      .= ((X (\) Z) (\/) (Y (\) Z)).i by A1,Def4;
end;

theorem Th73:
  (X (\) Y) (\) Z = X (\) (Y (\/) Z)
proof
    let i be object;
    assume
A1: i in I;
    hence ((X (\) Y) (\) Z).i = (X (\) Y).i \ Z.i by Def6
      .= X.i \ Y.i \ Z.i by A1,Def6
      .= X.i \ (Y.i \/ Z.i) by XBOOLE_1:41
      .= X.i \ (Y (\/) Z).i by A1,Def4
      .= (X (\) (Y (\/) Z)).i by A1,Def6;
end;

theorem
  (X (/\) Y) (\) Z = (X (\) Z) (/\) (Y (\) Z)
proof
A1: X (\) Z c= X by Th56;
  thus (X (/\) Y) (\) Z = (X (\) Z) (/\) Y by Th62
    .= (X (\) Z) (\) ((X (\) Z) (\) Y) by Th68
    .= (X (\) Z) (\) (X (\) (Z (\/) Y)) by Th73
    .= ((X (\) Z) (\) X) (\/) ((X (\) Z) (/\) (Z (\/) Y)) by Th64
    .= EmptyMS I (\/) ((X (\) Z) (/\) (Z (\/) Y)) by A1,Th52
    .= (X (\) Z) (/\) (Y (\/) Z) by Th22,Th43
    .= (X (\) Z) (/\) ((Y (\) Z) (\/) Z) by Th67
    .= (X (\) Z) (/\) (Y (\) Z) (\/) (X (\) Z) (/\) Z by Th32
    .= (X (\) Z) (/\) (Y (\) Z) (\/) EmptyMS I by Th63
    .= (X (\) Z) (/\) (Y (\) Z) by Th22,Th43;
end;

theorem Th75:
  (X (\/) Y) (\) Y = X (\) Y
proof
  thus (X (\/) Y) (\) Y = X (\) Y (\/) (Y (\) Y) by Th72
    .= X (\) Y (\/) EmptyMS I by Th52
    .= X (\) Y by Th22,Th43;
end;

theorem
  X c= Y (\/) Z implies X (\) Y c= Z & X (\) Z c= Y
proof
  assume
A1: X c= Y (\/) Z;
  then X (\) Y c= Z (\/) Y (\) Y by Th53;
  then
A2: X (\) Y c= Z (\) Y by Th75;
  Z (\) Y c= Z by Th56;
  hence X (\) Y c= Z by A2,Th13;
  X (\) Z c= Y (\/) Z (\) Z by A1,Th53;
  then
A3: X (\) Z c= Y (\) Z by Th75;
  Y (\) Z c= Y by Th56;
  hence thesis by A3,Th13;
end;

theorem Th77:
  (X (\/) Y) (\) (X (/\) Y) = (X (\) Y) (\/) (Y (\) X)
proof
  thus (X (\/) Y) (\) (X (/\) Y) = X (\) (X (/\) Y) (\/) (Y (\) (X (/\) Y))
          by Th72
    .= X (\) Y (\/) (Y (\) (X (/\) Y)) by Th70
    .= (X (\) Y) (\/) (Y (\) X) by Th70;
end;

theorem Th78:
  (X (\) Y) (\) Y = X (\) Y
proof
  thus (X (\) Y) (\) Y = X (\) (Y (\/) Y) by Th73
    .= X (\) Y;
end;

theorem
  X (\) (Y (\/) Z) = (X (\) Y) (/\) (X (\) Z)
proof
  thus X (\) (Y (\/) Z) = X (\) Y (\) Z by Th73
    .= (X (\) Y) (/\) X (\) Z by Th56,Th23
    .= (X (\) Y) (/\) (X (\) Z) by Th62;
end;

theorem
  X (\) Y = Y (\) X implies X = Y
proof
  assume X (\) Y = Y (\) X;
  hence X = Y (\) X (\/) Y (/\) X by Th65
    .= Y by Th65;
end;

theorem
  X (/\) (Y (\) Z) = X (/\) Y (\) X (/\) Z
proof
A1: X (/\) Y c= X by Th15;
  X (/\) Y (\) X (/\) Z = ((X (/\) Y) (\) X) (\/) ((X (/\) Y) (\) Z) by Th69
    .= EmptyMS I (\/) ((X (/\) Y) (\) Z) by A1,Th52
    .= (X (/\) Y) (\) Z by Th22,Th43;
  hence thesis by Th62;
end;

theorem
  X (\) Y c= Z implies X c= Y (\/) Z
proof
  assume
A1: X (\) Y c= Z;
  X (/\) Y c= Y by Th15;
  then X (/\) Y (\/) (X (\) Y) c= Y (\/) Z by A1,Th20;
  hence thesis by Th65;
end;

theorem
  X (\) Y c= X (\+\) Y by Th14;

theorem
  X (\+\) EmptyMS I = X
proof
  thus X (\+\) EmptyMS I = X (\/) (EmptyMS I (\) X) by Th59
    .= X (\/) EmptyMS I by Th60
    .= X by Th22,Th43;
end;

theorem
  X (\+\) X = EmptyMS I by Th52;

theorem
  X (\/) Y = (X (\+\) Y) (\/) X (/\) Y
proof
  thus X (\/) Y = ((X (\) Y) (\/) X (/\) Y) (\/) Y by Th65
    .= (X (\) Y) (\/) (X (/\) Y (\/) Y) by Th28
    .= (X (\) Y) (\/) Y by Th31
    .= (X (\) Y) (\/) ((Y (\) X) (\/) (Y (/\) X)) by Th65
    .= (X (\+\) Y) (\/) X (/\) Y by Th28;
end;

theorem Th87:
  X (\+\) Y = (X (\/) Y) (\) X (/\) Y
proof
  thus X (\+\) Y = (X (\) X (/\) Y) (\/) (Y (\) X) by Th70
    .= (X (\) X (/\) Y) (\/) (Y (\) X (/\) Y) by Th70
    .= (X (\/) Y) (\) X (/\) Y by Th72;
end;

theorem
  (X (\+\) Y) (\) Z = (X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z))
proof
  thus (X (\+\) Y) (\) Z = (X (\) Y (\) Z) (\/) (Y (\) X (\) Z) by Th72
    .= (X (\) (Y (\/) Z)) (\/) (Y (\) X (\) Z) by Th73
    .= (X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z)) by Th73;
end;

theorem
  X (\) (Y (\+\) Z) = X (\) (Y (\/) Z) (\/) X (/\) Y (/\) Z
proof
  thus X (\) (Y (\+\) Z) = X (\) ((Y (\/) Z) (\) Y (/\) Z) by Th87
    .= X (\) (Y (\/) Z) (\/) X (/\) (Y (/\) Z) by Th64
    .= X (\) (Y (\/) Z) (\/) X (/\) Y (/\) Z by Th29;
end;

theorem Th90:
  (X (\+\) Y) (\+\) Z = X (\+\) (Y (\+\) Z)
proof
  set S1 = X (\) (Y (\/) Z), S2 = Y (\) (X (\/) Z), S3 = Z (\) (X (\/) Y),
      S4 = X (/\) Y (/\)
  Z;
  thus (X (\+\) Y) (\+\) Z
      = (((X (\) Y) (\) Z) (\/) ((Y (\) X) (\) Z))
            (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))  by Th72
    .= ( S1 (\/) ((Y (\) X) (\) Z)) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))
                by Th73
    .= ( S1 (\/) S2) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X))) by Th73
    .= ( S1 (\/) S2) (\/) (Z (\) ((X (\/) Y) (\) (X (/\) Y))) by Th77
    .= (S1 (\/) S2) (\/) (S4 (\/) S3) by Th64
    .= (S1 (\/) S2 (\/) S4) (\/) S3 by Th28
    .= (S1 (\/) S4 (\/) S2) (\/) S3 by Th28
    .= (S1 (\/) S4) (\/) (S2 (\/) S3) by Th28
    .= (S1 (\/) X (/\) (Y (/\) Z)) (\/) (S2 (\/) S3) by Th29
    .= X (\) ((Y (\/) Z) (\) (Y (/\) Z)) (\/) (S2 (\/) S3) by Th64
    .= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) (S2 (\/) (Z (\) (Y (\/) X)))
               by Th77
    .= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) ((Y (\) (Z (\/) X))
              (\/) (Z (\) Y (\) X)) by Th73
    .= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) ((Y (\) Z (\) X)
         (\/) (Z (\) Y (\) X)) by Th73
    .= X (\+\) (Y (\+\) Z) by Th72;
end;

theorem
  X (\) Y c= Z & Y (\) X c= Z implies X (\+\) Y c= Z by Th16;

theorem Th92:
  X (\/) Y = X (\+\) (Y (\) X)
proof
  thus X (\/) Y = Y (\/) (X (\/) X)
    .= X (\/) Y (\/) X by Th28
    .= (X (\) Y) (\/) Y (\/) X by Th67
    .= (X (\) Y) (\/) (X (\/) Y) by Th28
    .= (X (\) Y) (\/) (X (\/) (Y (\) X)) by Th67
    .= (X (\) Y) (\/) X (/\) X (\/) (Y (\) X) by Th28
    .= (X (\) (Y (\) X)) (\/) (Y (\) X) by Th64
    .= X (\+\) (Y (\) X) by Th78;
end;

theorem Th93:
  X (/\) Y = X (\+\) (X (\) Y)
proof
A1: X (\) Y c= X by Th56;
  thus X (/\) Y = X (\) (X (\) Y) by Th68
    .= (X (\) (X (\) Y)) (\/) EmptyMS I by Th22,Th43
    .= X (\+\) (X (\) Y) by A1,Th52;
end;

theorem Th94:
  X (\) Y = X (\+\) (X (/\) Y)
proof
A1: X (/\) Y c= X by Th15;
  thus X (\) Y = X (\) (X (/\) Y) by Th70
    .= (X (\) (X (/\) Y)) (\/) EmptyMS I by Th22,Th43
    .= X (\+\) (X (/\) Y) by A1,Th52;
end;

theorem Th95:
  Y (\) X = X (\+\) (X (\/) Y)
proof
A1: X c= Y (\/) X by Th14;
  thus Y (\) X = ((Y (\/) X) (\) X) by Th75
    .= EmptyMS I (\/) ((Y (\/) X) (\) X) by Th22,Th43
    .= X (\+\) (X (\/) Y) by A1,Th52;
end;

theorem
  X (\/) Y = X (\+\) Y (\+\) X (/\) Y
proof
  thus X (\/) Y = X (\+\) (Y (\) X) by Th92
    .= X (\+\) (Y (\+\) X (/\) Y) by Th94
    .= X (\+\) Y (\+\) X (/\) Y by Th90;
end;

theorem
  X (/\) Y = X (\+\) Y (\+\) (X (\/) Y)
proof
  thus X (/\) Y = X (\+\) (X (\) Y) by Th93
    .= X (\+\) (Y (\+\) (X (\/) Y)) by Th95
    .= X (\+\) Y (\+\) (X (\/) Y) by Th90;
end;

begin :: Meeting and overlap(p?)ing

theorem
  X overlaps Y or X overlaps Z implies X overlaps Y (\/) Z
proof
  assume
A1: X overlaps Y or X overlaps Z;
  per cases by A1;
  suppose
    X overlaps Y;
    then consider x such that
A2: x in X and
A3: x in Y by Th11;
    x in Y (\/) Z by A3,Th7;
    hence thesis by A2,Th10;
  end;
  suppose
    X overlaps Z;
    then consider x such that
A4: x in X and
A5: x in Z by Th11;
    x in Y (\/) Z by A5,Th7;
    hence thesis by A4,Th10;
  end;
end;

theorem Th99:
  X overlaps Y & Y c= Z implies X overlaps Z
proof
  assume that
A1: X overlaps Y and
A2: Y c= Z;
  consider x such that
A3: x in X and
A4: x in Y by A1,Th11;
  x in Z by A2,A4,Th9;
  hence thesis by A3,Th10;
end;

theorem Th100:
  X overlaps Y & X c= Z implies Z overlaps Y
proof
  assume that
A1: X overlaps Y and
A2: X c= Z;
  consider x such that
A3: x in X and
A4: x in Y by A1,Th11;
  x in Z by A2,A3,Th9;
  hence thesis by A4,Th10;
end;

theorem Th101:
  X c= Y & Z c= V & X overlaps Z implies Y overlaps V
proof
  assume that
A1: X c= Y and
A2: Z c= V;
  assume X overlaps Z;
  then Y overlaps Z by A1,Th100;
  hence thesis by A2,Th99;
end;

theorem
  X overlaps Y (/\) Z implies X overlaps Y & X overlaps Z
proof
  assume X overlaps Y (/\) Z;
  then consider x such that
A1: x in X and
A2: x in Y (/\) Z by Th11;
  x in Y & x in Z by A2,Th8;
  hence thesis by A1,Th10;
end;

theorem
  X overlaps Z & X c= V implies X overlaps Z (/\) V
proof
  assume that
A1: X overlaps Z and
A2: X c= V;
  consider x such that
A3: x in X and
A4: x in Z by A1,Th11;
  x in V by A2,A3,Th9;
  then x in Z (/\) V by A4,Th8;
  hence thesis by A3,Th10;
end;

theorem
  X overlaps Y (\) Z implies X overlaps Y by Th56,Th99;

theorem
  Y does not overlap Z implies X (/\) Y does not overlap X (/\) Z
proof
  assume
A1: Y does not overlap Z;
  X (/\) Y c= Y & X (/\) Z c= Z by Th15;
  hence thesis by A1,Th101;
end;

theorem
  X overlaps Y (\) Z implies Y overlaps X (\) Z
proof
  assume
A1: X overlaps Y (\) Z;
  let i be object;
  assume
A2: i in I;
  then X.i meets (Y (\) Z).i by A1;
  then X.i meets Y.i \ Z.i by A2,Def6;
  then Y.i meets X.i \ Z.i by XBOOLE_1:81;
  hence thesis by A2,Def6;
end;

theorem Th107:
  X meets Y & Y c= Z implies X meets Z
proof
  assume that
A1: X meets Y and
A2: Y c= Z;
  consider i being object such that
A3: i in I and
A4: X.i meets Y.i by A1;
  take i;
  Y.i c= Z.i by A2,A3;
  hence thesis by A3,A4,XBOOLE_1:63;
end;

theorem Th108:
  Y misses X (\) Y
proof
  now
    let i be object;
    assume i in I;
    then (X (\) Y).i = X.i \ Y.i by Def6;
    hence Y.i misses (X (\) Y).i by XBOOLE_1:79;
  end;
  hence thesis;
end;

theorem
  X (/\) Y misses X (\) Y
proof
  X (/\) Y c= Y & X (\) Y misses Y by Th15,Th108;
  hence thesis by Th107;
end;

theorem
  X (/\) Y misses X (\+\) Y
proof
  now
    let i be object;
    assume i in I;
    then (X (/\) Y).i = X.i /\ Y.i & (X (\+\) Y).i = X.i \+\ Y.i by Def5,Th4;
    hence (X (/\) Y).i misses (X (\+\) Y).i by XBOOLE_1:103;
  end;
  hence thesis;
end;

theorem Th111:
  X misses Y implies X (/\) Y = EmptyMS I
proof
  assume
A1: X misses Y;
  now
    let i be object;
    assume
A2: i in I;
    then
A3: X.i misses Y.i by A1;
    thus (X (/\) Y).i = X.i /\ Y.i by A2,Def5
      .= {} by A3;
  end;
  hence thesis by Th6;
end;

theorem
  X <> EmptyMS I implies X meets X
proof
  X = X (/\) X;
  hence thesis by Th111;
end;

theorem
  X c= Y & X c= Z & Y misses Z implies X = EmptyMS I
proof
  assume
A1: X c= Y & X c= Z;
  assume Y misses Z;
  then Y (/\) Z = EmptyMS I by Th111;
  hence thesis by A1,Th17,Th44;
end;

theorem
  Z (\/) V = X (\/) Y & X misses Z & Y misses V implies X = V & Y = Z
proof
  assume
A1: Z (\/) V = X (\/) Y;
  assume X misses Z & Y misses V;
  then
A2: X (/\) Z = EmptyMS I & Y (/\) V = EmptyMS I by Th111;
  thus X = X (/\) (Z (\/) V) by Th23,A1,Th14
    .= X (/\) Z (\/) X (/\) V by Th32
    .= (X (\/) Y) (/\) V by A2,Th32
    .= V by A1,Th14,Th23;
  thus Y = Y (/\) (Z (\/) V) by Th23,A1,Th14
    .= Y (/\) Z (\/) Y (/\) V by Th32
    .= (X (\/) Y) (/\) Z by A2,Th32
    .= Z by A1,Th14,Th23;
end;

theorem Th115:
  X misses Y implies X (\) Y = X
proof
  assume
A1: X misses Y;
    let i be object;
    assume
A2: i in I;
    then
A3: (X (\) Y).i = X.i \ Y.i by Def6;
    X.i misses Y.i by A1,A2;
    hence (X (\) Y).i = X.i by A3,XBOOLE_1:83;
end;

theorem
  X misses Y implies (X (\/) Y) (\) Y = X
proof
  (X (\/) Y) (\) Y = X (\) Y by Th75;
  hence thesis by Th115;
end;

theorem
  X (\) Y = X implies X misses Y
proof
  assume
A1: X (\) Y = X;
  let i be object;
  assume i in I;
  then X.i \ Y.i = X.i by A1,Def6;
  hence thesis by XBOOLE_1:83;
end;

theorem
  X (\) Y misses Y (\) X
proof
  let i be object;
  assume i in I;
  then (X (\) Y).i = X.i \ Y.i & (Y (\) X).i = Y.i \ X.i by Def6;
  hence thesis by XBOOLE_1:82;
end;

begin :: Roughly speaking

definition
  let I,X,Y;
  pred X [= Y means

  for x st x in X holds x in Y;
  reflexivity;
end;

theorem
  X c= Y implies X [= Y
proof
  assume
A1: X c= Y;
  let x such that
A2: x in X;
  let i be object;
  assume
A3: i in I;
  then
A4: X.i c= Y.i by A1;
  x.i in X.i by A2,A3;
  hence thesis by A4;
end;

theorem
  X [= Y & Y [= Z implies X [= Z;

begin :: Non empty set of sorts

theorem
  EmptyMS {} in EmptyMS {};

theorem
  for X being ManySortedSet of {} holds X = {};

reserve I for non empty set,
  x,X,Y for ManySortedSet of I;

theorem
  X overlaps Y implies X meets Y
proof
  set i = the Element of I;
  assume X overlaps Y;
  then X.i meets Y.i;
  hence thesis;
end;

theorem Th124:
  not ex x st x in EmptyMS I
proof
  set i = the Element of I;
  given x such that
A1: x in EmptyMS I;
  x.i in EmptyMS I.i by A1;
  hence contradiction;
end;

theorem
  x in X & x in Y implies X (/\) Y <> EmptyMS I
by Th8,Th124;

theorem
  X does not overlap EmptyMS I
proof
  assume X overlaps EmptyMS I;
  then ex x st x in X & x in EmptyMS I by Th11;
  hence contradiction by Th124;
end;

theorem Th127:
  X (/\) Y = EmptyMS I implies X does not overlap Y
proof
  assume
A1: X (/\) Y = EmptyMS I;
  assume X overlaps Y;
  then consider x such that
A2: x in X & x in Y by Th11;
  x in X (/\) Y by A2,Th8;
  hence contradiction by A1,Th124;
end;

theorem
  X overlaps X implies X <> EmptyMS I
proof
  X = X (/\) X;
  hence thesis by Th127;
end;

begin :: Empty and non-empty ManySortedSets

reserve I for set,
  x,X,Y,Z for ManySortedSet of I;

definition
  let I be set;
  let X be ManySortedSet of I;
  redefine attr X is empty-yielding means  :: redefines empty-yielding (FUNCT_1, redefinition) → empty-yielding (RELAT_1, definition)

  for i being object st i in I holds X.i is empty;
  compatibility
  proof
    dom X = I by PARTFUN1:def 2;
    hence thesis;
  end;
  redefine attr X is non-empty means  :: redefines non-empty (FUNCT_1, redefinition) → non-empty (RELAT_1, definition)
  :Def13:
  for i being object st i in I holds X.i is non empty;
  compatibility
  proof
    dom X = I by PARTFUN1:def 2;
    hence thesis;
  end;
end;

registration
  let I be set;
  cluster empty-yielding for ManySortedSet of I;
  existence
  proof
    take EmptyMS I;
    let i be object;
    assume i in I;
    thus thesis;
  end;
  cluster non-empty for ManySortedSet of I;
  existence
  proof
    set e = the set;
    reconsider M = I --> {e} as ManySortedSet of I;
    take M;
    let i be object;
    assume i in I;
    hence thesis by FUNCOP_1:7;
  end;
end;

registration
  let I be non empty set;
  cluster non-empty -> non empty-yielding for ManySortedSet of I;
  coherence
  proof
    set i = the Element of I;
    let M be ManySortedSet of I;
    assume
A1: M is non-empty;
    take i;
    thus i in I;
    thus thesis by A1;
  end;
  cluster empty-yielding -> non non-empty for ManySortedSet of I;
  coherence;
end;

theorem
  X is empty-yielding iff X = EmptyMS I
proof
  hereby
    assume X is empty-yielding;
    then for i being object st i in I holds X.i = {};
    hence X = EmptyMS I by Th6;
  end;
  assume
A1: X = EmptyMS I;
  let i be object;
  assume i in I;
  thus thesis by A1;
end;

theorem
  Y is empty-yielding & X c= Y implies X is empty-yielding
proof
  assume
A1: Y is empty-yielding & X c= Y;
  let i be object;
  assume i in I;
  then X.i c= Y.i & Y.i is empty by A1;
  hence thesis;
end;

theorem Th131:
  X is non-empty & X c= Y implies Y is non-empty
proof
  assume
A1: X is non-empty & X c= Y;
  let i be object;
  assume i in I;
  then X.i c= Y.i & X.i is non empty by A1;
  hence thesis;
end;

theorem Th132:
  X is non-empty & X [= Y implies X c= Y
proof
  assume that
A1: X is non-empty and
A2: X [= Y;
  deffunc F(object) = X.$1;
A3: for i being object st i in I holds F(i) <> {} by A1;
  consider f being ManySortedSet of I such that
A4: for i being object st i in I holds f.i in F(i)
from KuratowskiFunction(A3);
  let i be object such that
A5: i in I;
  let e be object;
  deffunc G(object) = IFEQ(i,$1,e,f.$1);
  consider g being Function such that
A6: dom g = I and
A7: for u being object st u in I holds g.u = G(u) from FUNCT_1:sch 3;
  reconsider g as ManySortedSet of I by A6,PARTFUN1:def 2,RELAT_1:def 18;
A8: g.i = IFEQ(i,i,e,f.i) by A5,A7
    .= e by FUNCOP_1:def 8;
  assume
A9: e in X.i;
  g in X
  proof
    let u be object such that
A10: u in I;
    per cases;
    suppose
      u = i;
      hence thesis by A8,A9;
    end;
    suppose
A11:  u <> i;
      g.u = IFEQ(i,u,e,f.u) by A7,A10
        .= f.u by A11,FUNCOP_1:def 8;
      hence thesis by A4,A10;
    end;
  end;
  then g in Y by A2;
  hence thesis by A5,A8;
end;

theorem
  X is non-empty & X [= Y implies Y is non-empty
proof
  assume
A1: X is non-empty;
  assume X [= Y;
  then X c= Y by A1,Th132;
  hence thesis by A1,Th131;
end;

reserve X for non-empty ManySortedSet of I;

theorem
  ex x st x in X
proof
  deffunc F(object) = X.$1;
A1: for i being object st i in I holds F(i) <> {} by Def13;
  consider f being ManySortedSet of I such that
A2: for i being object st i in I holds f.i in F(i)
from KuratowskiFunction(A1);
  take f;
  let i be object;
  thus thesis by A2;
end;

theorem Th135:
  (for x holds x in X iff x in Y) implies X = Y
proof
  deffunc F(object) = X.$1;
A1: for i being object st i in I holds F(i) <> {} by Def13;
  consider f being ManySortedSet of I such that
A2: for i being object st i in I holds f.i in F(i)
    from KuratowskiFunction(A1);
  assume
A3: for x holds x in X iff x in Y;
  now
    let i be object such that
A4: i in I;
    now
      let e be object;
      deffunc G(object) = IFEQ(i,$1,e,f.$1);
      consider g being Function such that
A5:   dom g = I and
A6:   for u being object st u in I holds g.u = G(u) from FUNCT_1:sch 3;
      reconsider g as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18;
A7:   g.i = IFEQ(i,i,e,f.i) by A4,A6
        .= e by FUNCOP_1:def 8;
      hereby
        assume
A8:     e in X.i;
        g in X
        proof
          let u be object such that
A9:       u in I;
          per cases;
          suppose
            u = i;
            hence thesis by A7,A8;
          end;
          suppose
A10:        u <> i;
            g.u = IFEQ(i,u,e,f.u) by A6,A9
              .= f.u by A10,FUNCOP_1:def 8;
            hence thesis by A2,A9;
          end;
        end;
        then g in Y by A3;
        hence e in Y.i by A4,A7;
      end;
      assume
A11:  e in Y.i;
      g in Y
      proof
        let u be object such that
A12:    u in I;
        per cases;
        suppose
          u = i;
          hence thesis by A7,A11;
        end;
        suppose
A13:      u <> i;
          f in X by A2;
          then
A14:      f in Y by A3;
          g.u = IFEQ(i,u,e,f.u) by A6,A12
            .= f.u by A13,FUNCOP_1:def 8;
          hence thesis by A12,A14;
        end;
      end;
      then g in X by A3;
      hence e in X.i by A4,A7;
    end;
    hence X.i = Y.i by TARSKI:2;
  end;
  hence thesis;
end;

theorem
  (for x holds x in X iff x in Y & x in Z) implies X = Y (/\) Z
proof
  assume
A1: for x holds x in X iff x in Y & x in Z;
  now
    let x;
    hereby
      assume x in X;
      then x in Y & x in Z by A1;
      hence x in Y (/\) Z by Th8;
    end;
    assume x in Y (/\) Z;
    then x in Y & x in Z by Th8;
    hence x in X by A1;
  end;
  hence thesis by Th135;
end;

begin :: Addenda

scheme
  MSSEx { I() -> set, P[object,object] }:
  ex f being ManySortedSet of I() st
   for i being object st i in I() holds P[i,f.i]
provided
A1: for i being object st i in I() ex j being object st P[i,j]
proof
  consider f being Function such that
A2: dom f = I() and
A3: for i being object st i in I() holds P[i,f.i] from CLASSES1:sch 1(A1);
  reconsider f as ManySortedSet of I() by A2,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A3;
end;

scheme
  MSSLambda { I() -> set, F(object) -> object }:
ex f being ManySortedSet of I() st
  for i being object st i in I() holds f.i = F(i);
  consider f being Function such that
A1: dom f = I() and
A2: for i being object st i in I() holds f.i = F(i) from FUNCT_1:sch 3;
  reconsider f as ManySortedSet of I() by A1,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A2;
end;

registration
  let I be set;
  cluster Function-yielding for ManySortedSet of I;
  existence
  proof
    set f = the Function;
    reconsider F = I --> f as ManySortedSet of I;
    take F;
    let x be object;
    assume x in dom F;
    thus thesis;
  end;
end;

definition
  let I be set;
  mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;

theorem
  not ex M being non-empty ManySortedSet of I st {} in rng M
proof
  let M be non-empty ManySortedSet of I;
A1: dom M = I by PARTFUN1:def 2;
  assume {} in rng M;
  then ex i being object st i in I & M.i = {} by A1,FUNCT_1:def 3;
  hence contradiction by Def13;
end;

definition
  let M be Function;
  mode Component of M is Element of rng M;
end;

theorem
  for I being non empty set for M being ManySortedSet of I, A being
  Component of M ex i being object st i in I & A = M.i
proof
  let I be non empty set;
  let M be ManySortedSet of I, A be Component of M;
A1: dom M = I by PARTFUN1:def 2;
  then rng M <> {} by RELAT_1:42;
  hence thesis by A1,FUNCT_1:def 3;
end;

theorem
  for M being ManySortedSet of I, i st i in I holds M.i is Component of M
proof
  let M be ManySortedSet of I, i;
  assume
A1: i in I;
  dom M = I by PARTFUN1:def 2;
  hence thesis by A1,FUNCT_1:def 3;
end;

definition
  let I;
  let B be ManySortedSet of I;
  mode Element of B -> ManySortedSet of I means
    for i being object st i in I holds it.i is Element of B.i;
  existence
  proof
    defpred Q[object,object] means $2 is Element of B.$1;
A1: for i being object st i in I ex j being object st Q[i,j]
    proof
      let i be object such that
      i in I;
      set j = the Element of B.i;
      reconsider j as set;
      take j;
      thus thesis;
    end;
    thus ex f being ManySortedSet of I st
     for i being object st i in I holds Q[i,f.i] from
    MSSEx(A1);
  end;
end;

begin :: Many Sorted Functions

definition
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  mode ManySortedFunction of A,B -> ManySortedSet of I means
:Def15: for i st i in I holds it.i is Function of A.i, B.i;
  correctness
  proof
    defpred P[object,object] means $2 is Function of A.$1,B.$1;
A1: for i being object st i in I ex j being object st P[i,j]
    proof
      let i be object such that
      i in I;
      set j = the Function of A.i,B.i;
      reconsider j as set;
      take j;
      thus thesis;
    end;
    consider f being ManySortedSet of I such that
A2: for i being object st i in I holds P[i,f.i] from MSSEx(A1);
    f is Function-yielding
    proof
      let i be object;
      assume i in dom f;
      then i in I by PARTFUN1:def 2;
      hence thesis by A2;
    end;
    then reconsider f as ManySortedFunction of I;
    take f;
    let i;
    assume i in I;
    hence thesis by A2;
  end;
end;

registration
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  cluster ->Function-yielding for ManySortedFunction of A,B;
  coherence
  proof
    let f be ManySortedFunction of A,B;
    let i be object;
    assume i in dom f;
    then i in I by PARTFUN1:def 2;
    hence thesis by Def15;
  end;
end;

registration
  let I be set;
  let J be non empty set;
  let O be Function of I,J;
  let F be ManySortedSet of J;
  cluster F*O -> total for I-defined Function;
  coherence
  proof
A1: dom F = J by PARTFUN1:def 2;
    rng O c= J & dom O = I by FUNCT_2:def 1,RELAT_1:def 19;
    then dom(F*O) = I by A1,RELAT_1:27;
    hence thesis by PARTFUN1:def 2;
  end;
end;

reserve D for non empty set,
  n for Nat;

scheme
  LambdaDMS {D()->non empty set, F(object)->object}:
  ex X be ManySortedSet of D() st
  for d be Element of D() holds X.d = F(d) proof
  consider f be Function such that
A1: dom f = D() and
A2: for d be Element of D() holds f.d = F(d) from FUNCT_1:sch 4;
  f is ManySortedSet of D() by A1,PARTFUN1:def 2,RELAT_1:def 18;
  hence thesis by A2;
end;

registration
  let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J;
  cluster B.j -> non empty;
  coherence by Def13;
end;

reserve X,Y for ManySortedSet of I;

definition
  let I, X,Y;
  func [|X,Y|] -> ManySortedSet of I means
  for i being object st i in I holds it.i = [:X.i,Y.i:];
  existence
  proof
    deffunc F(object) = [:X.$1,Y.$1:];
    consider f be Function such that
A1: dom f = I &
   for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
    reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be ManySortedSet of I;
    assume that
A2: for i being object st i in I holds f.i = [:X.i,Y.i:] and
A3: for i being object st i in I holds g.i = [:X.i,Y.i:];
    for x be object st x in I holds f.x = g.x
    proof
      let x be object;
      assume
A4:   x in I;
      then f.x = [:X.x,Y.x:] by A2;
      hence thesis by A3,A4;
    end;
    hence thesis;
  end;
end;

definition
  let I, X, Y;
  deffunc F(object) = Funcs(X.$1,Y.$1);
  func (Funcs) (X,Y) -> ManySortedSet of I means
  for i being object st i in I holds it.i = Funcs(X.i,Y.i);
  existence
  proof
    thus ex M being ManySortedSet of I st
    for i being object st i in I holds M.i = F(i) from MSSLambda;
  end;
  uniqueness
  proof
    let F1, F2 be ManySortedSet of I such that
A1: for i being object st i in I holds F1.i = Funcs(X.i, Y.i) and
A2: for i being object st i in I holds F2.i = Funcs(X.i, Y.i);
    now
      let i be object;
      assume
A3:   i in I;
      hence F1.i = Funcs(X.i, Y.i) by A1
        .= F2.i by A2,A3;
    end;
    hence thesis;
  end;
end;

definition
  let I be set, M be ManySortedSet of I;
  mode ManySortedSubset of M -> ManySortedSet of I means
  :Def18:
  it c= M;
  existence;
end;

registration
  let I be set, M be non-empty ManySortedSet of I;
  cluster non-empty for ManySortedSubset of M;
  existence
  proof
    reconsider N= M as ManySortedSubset of M by Def18;
    take N;
    thus thesis;
  end;
end;

definition
  let F,G be Function-yielding Function;
  func G**F -> Function means
  :Def19:
  dom it = (dom F) /\ (dom G) &
  for i be object st i in dom it holds it.i = (G.i)*(F.i);
  existence
  proof
    defpred P[object,object] means $2 = (G.$1)*(F.$1);
A1: for i be object st i in dom F /\ dom G ex u be object st P[i,u];
    ex H being Function st
    dom H = dom F /\ dom G & for i be object st i in dom F /\ dom G holds
    P[i,H.i] from CLASSES1:sch 1(A1);
    hence thesis;
  end;
  uniqueness
  proof
    let H1,H2 be Function;
    assume that
A2: dom H1 = dom F /\ dom G and
A3: for i be object st i in dom H1 holds H1.i = (G.i)*(F.i) and
A4: dom H2 = dom F /\ dom G and
A5: for i be object st i in dom H2 holds H2.i = (G.i)*(F.i);
    now
      let i be object;
      reconsider f = F.i as Function;
      reconsider g = G.i as Function;
      assume
A6:   i in dom F /\ dom G;
      then H1.i = g*f by A2,A3;
      hence H1.i = H2.i by A4,A5,A6;
    end;
    hence thesis by A2,A4;
  end;
end;

registration
  let F,G be Function-yielding Function;
  cluster G**F -> Function-yielding;
  coherence
  proof
    set H = G**F;
    let x be object;
    reconsider f = F.x as Function;
    reconsider g = G.x as Function;
    assume x in dom H;
    then H.x = g*f by Def19;
    hence thesis;
  end;
end;

definition
  let I be set, A be ManySortedSet of I, F be ManySortedFunction of I;
  func F.:.:A -> ManySortedSet of I means
  for i be set st i in I holds it.i = (F.i).:(A.i);
  existence
  proof
    defpred P[object,object] means $2 = (F.$1).:(A.$1);
A1: for i be object st i in I ex u be object st P[i,u];
    consider g being Function such that
A2: dom g = I & for i be object st i in I holds P[i,g.i] from CLASSES1:
    sch 1( A1);
    reconsider g as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
    take g;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let B,B1 be ManySortedSet of I;
    assume that
A3: for i be set st i in I holds B.i = (F.i).:(A.i) and
A4: for i be set st i in I holds B1.i = (F.i).:(A.i);
    now
      let i be object;
      reconsider f = F.i as Function;
      assume
A5:   i in I;
      then B.i = f.:(A.i) by A3;
      hence B.i = B1.i by A4,A5;
    end;
    hence thesis;
  end;
end;

registration
  let I;
  cluster EmptyMS I -> empty-yielding;
  coherence;
end;

scheme
  MSSExD { I() -> non empty set, P[object,object] }:
  ex f being ManySortedSet of I()
  st for i being Element of I() holds P[i,f.i]
provided
A1: for i being Element of I() ex j being object st P[i,j];
A2: for i being object st i in I() ex j being object st P[i,j] by A1;
  consider f being ManySortedSet of I() such that
A3: for i being object st i in I() holds P[i,f.i] from MSSEx(A2);
  take f;
  let i be Element of I();
  thus thesis by A3;
end;

registration
  let A be non empty set;
  cluster non-empty -> non empty-yielding for ManySortedSet of A;
  coherence;
end;

registration
  let X be non empty set;
  cluster -> non empty for ManySortedSet of X;
  coherence;
end;

theorem
  for F, G, H be Function-yielding Function holds
  (H ** G) ** F = H ** (G ** F)
proof
  let F, G, H be Function-yielding Function;
  set f = (H ** G) ** F, g = H ** (G ** F);
  now
A1: dom f = (dom (H ** G)) /\ dom F by Def19
      .= (dom H) /\ (dom G) /\ (dom F) by Def19;
    then
A2: dom f = (dom H) /\ ((dom G) /\ dom F) by XBOOLE_1:16;
    hence
A3: dom f = (dom H) /\ (dom (G ** F)) by Def19
      .= dom g by Def19;
    let x be object;
    assume
A4: x in dom f;
    then x in (dom H) /\ (dom G) by A1,XBOOLE_0:def 4;
    then
A5: x in dom (H ** G) by Def19;
    x in (dom G) /\ (dom F) by A2,A4,XBOOLE_0:def 4;
    then
A6: x in dom (G ** F) by Def19;
    thus f.x = ((H**G).x) * (F.x) by A4,Def19
      .= (H.x)*(G.x)*(F.x) by A5,Def19
      .= (H.x)*((G.x)*(F.x)) by RELAT_1:36
      .= (H.x)*((G**F).x) by A6,Def19
      .= g.x by A3,A4,Def19;
  end;
  hence thesis;
end;

registration
 let I be set, f be non-empty ManySortedSet of I;
 cluster total for I-defined f-compatible Function;
  existence
  proof
    deffunc F(object) = f.$1;
A1: for e being object st e in I holds F(e) <> {};
   consider g being ManySortedSet of I such that
A2:  for e being object st e in I holds g.e in F(e)
from KuratowskiFunction(A1);
    g is f-compatible
    proof let x be object;
     assume x in dom g;
      then x in I by PARTFUN1:def 2;
     hence g.x in f.x by A2;
    end;
    then reconsider g as I-defined f-compatible Function;
   take g;
   thus g is total;
  end;
end;

theorem
 for I being set, f being non-empty ManySortedSet of I
 for p being f-compatible I-defined Function
  ex s being f-compatible ManySortedSet of I st p c= s
 proof
  let I be set, f being non-empty ManySortedSet of I;
  let p be f-compatible I-defined Function;
   set h = the (f)-compatible ManySortedSet of I;
  take h+*p;
  thus p c= h+*p by FUNCT_4:25;
 end;

theorem
  for I,A be set
  for s,ss being ManySortedSet of I
  holds (ss +* s | A) | A = s | A
proof
  let I,A be set;
  let s,ss be ManySortedSet of I;
  dom s = I by PARTFUN1:def 2
    .= dom ss by PARTFUN1:def 2;
  then A /\ dom ss c= A /\ dom s;
  hence thesis by FUNCT_4:88;
end;

registration
 let X be non empty set, Y be set;
 cluster X-valued for ManySortedSet of Y;
 existence
  proof
   take M = Y --> the Element of X;
A1:  {the Element of X} c= X by ZFMISC_1:31;
    rng M c= {the Element of X} by FUNCOP_1:13;
   hence rng M c= X by A1;
  end;
end;

theorem
  for I,Y being non empty set, M be Y-valued ManySortedSet of I,
     x be Element of I
  holds M.x = M/.x
proof
  let I,Y be non empty set, M be Y-valued ManySortedSet of I,
     x be Element of I;
  dom M = I by PARTFUN1:def 2;
  hence M.x = M/.x by PARTFUN1:def 6;
end;

theorem
 for f being Function, M being ManySortedSet of I
   holds (f+*M)|I = M
proof
 let f be Function, M be ManySortedSet of I;
A1: dom(f|I) c= I by RELAT_1:58;
A2: dom M = I by PARTFUN1:def 2;
 thus (f+*M)|I = f|I +* M|I by FUNCT_4:71
   .= f|I +* M
   .= M by A1,A2,FUNCT_4:19;
end;

theorem
 for I being set, Y being non empty set
 for p being Y-valued I-defined Function
  ex s being Y-valued ManySortedSet of I st p c= s
 proof
  let I be set, Y being non empty set;
  let p be Y-valued I-defined Function;
   set h = the Y-valued ManySortedSet of I;
  take h+*p;
  thus p c= h+*p by FUNCT_4:25;
 end;

theorem
 X c= Y & Y c= X implies X = Y by Lm1;

definition let I be non empty set, A,B be ManySortedSet of I;
 redefine pred A = B means  :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  for i being Element of I holds A.i = B.i;
 compatibility;
end;

registration
  let X be with_non-empty_elements set;
  cluster id X -> non-empty;
  coherence by SETFAM_1:def 8;
end;

scheme
  MSSLambda { I() -> set, F(object) -> object }:
  ex f being ManySortedSet of I() st
  for i being set st i in I() holds f.i = F(i);
  consider f being Function such that
A1: dom f = I() and
A2: for i being object st i in I() holds f.i = F(i) from FUNCT_1:sch 3;
  reconsider f as ManySortedSet of I() by A1,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A2;
end;