:: Manysorted Sets
::  by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-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 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;
 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;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SETFAM_1, FUNCOP_1;
 theorems TARSKI, FUNCOP_1, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1, FUNCT_2,
      PARTFUN1, FUNCT_4, ZFMISC_1;
 schemes FUNCT_1, CLASSES1, XBOOLE_0;

begin

reserve i,j,e,u for set;

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
      hereby
        let i;
        assume i in rng f;
        then ex e st e in dom f & f.e = i by FUNCT_1:def 3;
        then i = {} by A1;
        hence i in { {} } by TARSKI:def 1;
      end;
      set e = the Element of dom f;
      let i;
      assume i in { {} };
      then
A3:   i = {} by TARSKI:def 1;
A4:   dom f <> {} by A2,RELAT_1:41;
      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 st i in dom f holds f.i is empty by RELAT_1:38;
  end;
  suppose
A6: rng f = { {} };
    let i;
    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(set) -> set}:
 ex f being ManySortedSet of A() st for e st e in A() holds f.e in F(e)
provided
A1: for e st e in A() holds F(e) <> {}
proof
  defpred P[set,set] means $2 in F($1);
A2: now
    let e;
    set fe = the Element of F(e);
    assume
A3: e in A();
    reconsider fe as set;
    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 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
  :Def1:
  for i st i in I holds X.i in Y.i;
  pred X c= Y means
  :Def2:
  for i 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;
  asymmetry
  proof
    let X,Y be ManySortedSet of I;
    assume
A1: for i 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 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 by Def1;
  end;
end;

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

theorem Th3:
  (for i 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 by FUNCT_1:2;
end;

definition
  let I;
  func [[0]]I -> ManySortedSet of I equals
  I --> {};
  coherence;
  correctness;
  let X,Y;
  func X \/ Y -> ManySortedSet of I means
  :Def4:
  for i st i in I holds it.i = X.i \/ Y.i;
  existence
  proof
    deffunc F(set) = X.$1 \/ Y.$1;
    consider f being Function such that
A1: dom f = I and
A2: for i 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 st i in I holds A1.i = X.i \/ Y.i and
A4: for i st i in I holds A2.i = X.i \/ Y.i;
    now
      let i;
      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 st i in I holds it.i = X.i /\ Y.i;
  existence
  proof
    deffunc F(set) = X.$1 /\ Y.$1;
    consider f being Function such that
A6: dom f = I and
A7: for i 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 st i in I holds A1.i = X.i /\ Y.i and
A9: for i st i in I holds A2.i = X.i /\ Y.i;
    now
      let i;
      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 st i in I holds it.i = X.i \ Y.i;
  existence
  proof
    deffunc F(set) = X.$1 \ Y.$1;
    consider f being Function such that
A11: dom f = I and
A12: for i 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 st i in I holds A1.i = X.i \ Y.i and
A14: for i st i in I holds A2.i = X.i \ Y.i;
    now
      let i;
      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
  :Def7:
  for i st i in I holds X.i meets Y.i;
  symmetry;
  pred X misses Y means
  :Def8:
  for i 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 Th5:
  [[0]]I.i = {}
proof
  per cases;
  suppose
    i in I;
    hence thesis by FUNCOP_1:7;
  end;
  suppose
    not i in I;
    then not i in dom [[0]]I by FUNCOP_1:13;
    hence thesis by FUNCT_1:def 2;
  end;
end;

theorem Th6:
  (for i st i in I holds X.i = {}) implies X = [[0]]I
proof
  assume
A1: for i st i in I holds X.i = {};
  now
    let i;
    assume i in I;
    hence X.i = {} by A1
      .= [[0]]I.i by Th5;
  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;
  assume
A2: i in I;
  then x.i in X.i or x.i in Y.i by A1,Def1;
  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;
      assume
A2:   i in I;
      then x.i in (X /\ Y).i by A1,Def1;
      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;
      assume
A3:   i in I;
      then x.i in (X /\ Y).i by A1,Def1;
      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;
  assume
A5: i in I;
  then x.i in X.i & x.i in Y.i by A4,Def1;
  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;
  assume i in I;
  then x.i in X.i & X.i c= Y.i by A1,Def1,Def2;
  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;
  assume i in I;
  then x.i in X.i & x.i in Y.i by A1,Def1;
  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(set) = X.$1 /\ Y.$1;
  assume
A1: X overlaps Y;
A2: now
    let i;
    assume i in I;
    then X.i meets Y.i by A1,Def7;
    hence F(i) <> {} by XBOOLE_0:def 7;
  end;
  consider x being ManySortedSet of I such that
A3: for i st i in I holds x.i in F(i) from KuratowskiFunction(A2);
  take x;
  now
    let i;
    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 by Def1;
  now
    let i;
    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 by Def1;
end;

theorem
  x in X \ Y implies x in X
proof
  assume
A1: x in X \ Y;
  thus x in X
  proof
    let i;
    assume
A2: i in I;
    then x.i in (X \ Y).i by A1,Def1;
    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
A1: X c= Y & Y c= X;
    now
      let i;
      assume i in I;
      then X.i c= Y.i & Y.i c= X.i by A1,Def2;
      hence X.i = Y.i by XBOOLE_0:def 10;
    end;
    hence thesis by Th3;
  end;

definition
  let I,X,Y;
  redefine pred X = Y means
  for i 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 such that
A3: i in I;
  let e;
  assume
A4: e in X.i;
  X.i c= Y.i by A1,A3,Def2;
  then
A5: e in Y.i by A4;
  Y.i c= Z.i by A2,A3,Def2;
  hence thesis by A5;
end;

theorem Th14:
  X c= X \/ Y
proof
    let i such that
A1: i in I;
    let e;
    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 such that
A1: i in I;
    let e;
    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;
  assume
A2: i in I;
  then X.i c= Z.i & Y.i c= Z.i by A1,Def2;
  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;
  assume
A2: i in I;
  then Z.i c= X.i & Z.i c= Y.i by A1,Def2;
  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;
    assume
A2: i in I;
    then
A3: X.i c= Z.i by A1,Def2;
    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;
    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;
    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;
    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:
  [[0]]I c= X
proof
  let i such that
A1: i in I;
  let e;
  assume e in [[0]]I.i;
  hence thesis by A1,FUNCOP_1:7;
end;

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

theorem
  X c= Y & X c= Z & Y /\ Z = [[0]]I implies X = [[0]]I by Th17,Th44;

theorem
  X c= Y & Y /\ Z = [[0]]I implies X /\ Z = [[0]]I by Th44,Th19;

theorem
  X \/ [[0]]I = X & [[0]]I \/ X = X by Th22,Th43;

theorem
  X \/ Y = [[0]]I implies X = [[0]]I by Th44,Th14;

theorem
  X /\ [[0]]I = [[0]]I by Th23,Th43;

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

theorem
  Y c= X & X /\ Y = [[0]]I implies Y = [[0]]I by Th23;

begin :: Difference and symmetric difference

theorem Th52:
  X \ Y = [[0]]I iff X c= Y
proof
  hereby
    assume
A1: X \ Y = [[0]]I;
    now
      let i;
      assume i in I;
      then X.i \ Y.i = (X \ Y).i by Def6
        .= {} by A1,Th5;
      hence X.i c= Y.i by XBOOLE_1:37;
    end;
    hence X c= Y by Def2;
  end;
  assume
A2: X c= Y;
  now
    let i;
    assume
A3: i in I;
    then
A4: X.i c= Y.i by A2,Def2;
    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;
    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,Def2;
    hence (X \ Z).i c= (Y \ Z).i by A3,XBOOLE_1:33;
  end;
  hence thesis by Def2;
end;

theorem Th54:
  X c= Y implies Z \ Y c= Z \ X
proof
  assume
A1: X c= Y;
  now
    let i;
    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,Def2;
    hence (Z \ Y).i c= (Z \ X).i by A3,XBOOLE_1:34;
  end;
  hence thesis by Def2;
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 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 by Def2;
end;

theorem
  X c= Y \ X implies X = [[0]]I
proof
  assume
A1: X c= Y \ X;
    let i;
    assume
A2: i in I;
    then X.i c= (Y \ X).i by A1,Def2;
    then X.i c= Y.i \ X.i by A2,Def6;
    hence X.i = {} by XBOOLE_1:38
      .= [[0]]I.i by Th5;
end;

theorem
  X \ X = [[0]]I by Th52;

theorem Th59:
  X \ [[0]]I = X
proof
    let i;
    assume i in I;
    hence (X \ [[0]]I).i = X.i \ [[0]]I.i by Def6
      .= X.i \ {} by Th5
      .= X.i;
end;

theorem Th60:
  [[0]]I \ X = [[0]]I
proof
  [[0]]I c= X by Th43;
  hence thesis by Th52;
end;

theorem
  X \ (X \/ Y) = [[0]]I
proof
  X c= X \/ Y by Th14;
  hence thesis by Th52;
end;

theorem Th62:
  X /\ (Y \ Z) = (X /\ Y) \ Z
proof
    let i;
    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 = [[0]]I
proof
A1: Y /\ X c= Y by Th15;
  thus (X \ Y) /\ Y = (Y /\ X) \ Y by Th62
    .= [[0]]I by A1,Th52;
  thus thesis;
end;

theorem Th64:
  X \ (Y \ Z) = (X \ Y) \/ X /\ Z
proof
    let i;
    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 \ [[0]]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
    .= [[0]]I \/ X /\ Y by Th52
    .= X /\ Y by Th22,Th43;
end;

theorem Th69:
  X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof
    let i;
    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
    .= [[0]]I \/ (X \ Y) by Th52
    .= X \ Y by Th22,Th43;
end;

theorem
  X /\ Y = [[0]]I iff X \ Y = X
proof
  hereby
    assume
A1: X /\ Y = [[0]]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;
    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;
    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
    .= [[0]]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) \/ [[0]]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 \/ [[0]]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
    .= [[0]]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 \+\ [[0]]I = X
proof
  thus X \+\ [[0]]I = X \/ ([[0]]I \ X) by Th59
    .= X \/ [[0]]I by Th60
    .= X by Th22,Th43;
end;

theorem
  X \+\ X = [[0]]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)) \/ [[0]]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)) \/ [[0]]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
    .= [[0]]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;
  assume
A2: i in I;
  then X.i meets (Y \ Z).i by A1,Def7;
  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 such that
A3: i in I and
A4: X.i meets Y.i by A1,Def8;
  take i;
  Y.i c= Z.i by A2,A3,Def2;
  hence thesis by A3,A4,XBOOLE_1:63;
end;

theorem Th108:
  Y misses X \ Y
proof
  now
    let i;
    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 by Def8;
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;
    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 by Def8;
end;

theorem Th111:
  X misses Y implies X /\ Y = [[0]]I
proof
  assume
A1: X misses Y;
  now
    let i;
    assume
A2: i in I;
    then
A3: X.i misses Y.i by A1,Def8;
    thus (X /\ Y).i = X.i /\ Y.i by A2,Def5
      .= {} by A3,XBOOLE_0:def 7;
  end;
  hence thesis by Th6;
end;

theorem
  X <> [[0]]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 = [[0]]I
proof
  assume
A1: X c= Y & X c= Z;
  assume Y misses Z;
  then Y /\ Z = [[0]]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 = [[0]]I & Y /\ V = [[0]]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;
    assume
A2: i in I;
    then
A3: (X \ Y).i = X.i \ Y.i by Def6;
    X.i misses Y.i by A1,A2,Def8;
    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;
  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;
  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
  :Def11:
  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;
  assume
A3: i in I;
  then
A4: X.i c= Y.i by A1,Def2;
  x.i in X.i by A2,A3,Def1;
  hence thesis by A4;
end;

theorem
  X [= Y & Y [= Z implies X [= Z
proof
  assume that
A1: X [= Y and
A2: Y [= Z;
  let x;
  assume x in X;
  then x in Y by A1,Def11;
  hence thesis by A2,Def11;
end;

begin :: Non empty set of sorts

theorem
  [[0]]{} in [[0]]{}
proof
  let i;
  thus thesis;
end;

theorem
  for X being ManySortedSet of {} holds X = {}
proof
  let X be ManySortedSet of {};
  dom X = {} by PARTFUN1:def 2;
  hence thesis by RELAT_1:41;
end;

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 by Def7;
  hence thesis by Def8;
end;

theorem Th124:
  not ex x st x in [[0]]I
proof
  set i = the Element of I;
  given x such that
A1: x in [[0]]I;
  x.i in [[0]]I.i by A1,Def1;
  hence contradiction by FUNCOP_1:7;
end;

theorem
  x in X & x in Y implies X /\ Y <> [[0]]I
proof
  assume x in X & x in Y;
  then x in X /\ Y by Th8;
  hence thesis by Th124;
end;

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

theorem Th127:
  X /\ Y = [[0]]I implies X does not overlap Y
proof
  assume
A1: X /\ Y = [[0]]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 <> [[0]]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

  for i st i in I holds X.i is
  empty;
  compatibility
  proof
    dom X = I by PARTFUN1:def 2;
    hence thesis by FUNCT_1:def 8;
  end;
  redefine attr X is non-empty means
  :Def13:
  for i st i in I holds X.i is non empty;
  compatibility
  proof
    dom X = I by PARTFUN1:def 2;
    hence thesis by FUNCT_1:def 9;
  end;
end;

registration
  let I be set;
  cluster empty-yielding for ManySortedSet of I;
  existence
  proof
    take [[0]]I;
    let i;
    assume i in I;
    thus thesis by Th5;
  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;
    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,Def13;
  end;
  cluster empty-yielding -> non non-empty for ManySortedSet of I;
  coherence;
end;

theorem
  X is empty-yielding iff X = [[0]]I
proof
  hereby
    assume X is empty-yielding;
    then for i st i in I holds X.i = {};
    hence X = [[0]]I by Th6;
  end;
  assume
A1: X = [[0]]I;
  let i;
  assume i in I;
  thus thesis by A1,Th5;
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;
  assume i in I;
  then X.i c= Y.i & Y.i is empty by A1,Def2;
  hence thesis by XBOOLE_1:3;
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;
  assume i in I;
  then X.i c= Y.i & X.i is non empty by A1,Def2,Def13;
  hence thesis by XBOOLE_1:3;
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(set) = X.$1;
A3: for i st i in I holds F(i) <> {} by A1,Def13;
  consider f being ManySortedSet of I such that
A4: for i st i in I holds f.i in F(i) from KuratowskiFunction(A3);
  let i such that
A5: i in I;
  let e;
  deffunc G(set) = IFEQ(i,$1,e,f.$1);
  consider g being Function such that
A6: dom g = I and
A7: for u 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 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,Def11;
  hence thesis by A5,A8,Def1;
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(set) = X.$1;
A1: for i st i in I holds F(i) <> {} by Def13;
  consider f being ManySortedSet of I such that
A2: for i st i in I holds f.i in F(i) from KuratowskiFunction(A1);
  take f;
  let i;
  thus thesis by A2;
end;

theorem Th135:
  (for x holds x in X iff x in Y) implies X = Y
proof
  deffunc F(set) = X.$1;
A1: for i st i in I holds F(i) <> {} by Def13;
  consider f being ManySortedSet of I such that
A2: for i 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 such that
A4: i in I;
    now
      let e;
      deffunc G(set) = IFEQ(i,$1,e,f.$1);
      consider g being Function such that
A5:   dom g = I and
A6:   for u 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 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,Def1;
      end;
      assume
A11:  e in Y.i;
      g in Y
      proof
        let u 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,Def1;
          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,Def1;
        end;
      end;
      then g in X by A3;
      hence e in X.i by A4,A7,Def1;
    end;
    hence X.i = Y.i by TARSKI:1;
  end;
  hence thesis by Th3;
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[set,set] }: ex f being ManySortedSet of I() st for i
  st i in I() holds P[i,f.i]
provided
A1: for i st i in I() ex j st P[i,j]
proof
A2: for i st i in I() ex j st P[i,j] by A1;
  consider f being Function such that
A3: dom f = I() and
A4: for i st i in I() holds P[i,f.i] from CLASSES1:sch 1(A2);
  reconsider f as ManySortedSet of I() by A3,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A4;
end;

scheme
  MSSLambda { I() -> set, F(set) -> set }: ex f being ManySortedSet of I() st
  for i st i in I() holds f.i = F(i) proof
  consider f being Function such that
A1: dom f = I() and
A2: for i 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 set;
    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 st i in I & M.i = {} by A1,FUNCT_1:def 3;
  hence contradiction by Def13;
end;

definition
  let I be set;
  let M be ManySortedSet of I;
  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 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 st i in I holds it.i is
    Element of B.i;
  existence
  proof
    defpred Q[set,set] means $2 is Element of B.$1;
A1: for i st i in I ex j st Q[i,j]
    proof
      let i 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 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[set,set] means $2 is Function of A.$1,B.$1;
A1: for i st i in I ex j st P[i,j]
    proof
      let i 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 st i in I holds P[i,f.i] from MSSEx(A1);
    f is Function-yielding
    proof
      let i;
      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 set;
    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(set)->set}: 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 st i in I holds it.i = [:X.i,Y.i:];
  existence
  proof
    deffunc F(set) = [:X.$1,Y.$1:];
    consider f be Function such that
A1: dom f = I & for i 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 st i in I holds f.i = [:X.i,Y.i:] and
A3: for i st i in I holds g.i = [:X.i,Y.i:];
    for x be set st x in I holds f.x = g.x
    proof
      let x be set;
      assume
A4:   x in I;
      then f.x = [:X.x,Y.x:] by A2;
      hence thesis by A3,A4;
    end;
    hence thesis by Th3;
  end;
end;

definition
  let I, X, Y;
  deffunc F(set) = Funcs(X.$1,Y.$1);
  func (Funcs) (X,Y) -> ManySortedSet of I means
  for i be set st i in I holds it.i = Funcs(X.i,Y.i);
  existence
  proof
    thus ex M being ManySortedSet of I st for i be set 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 be set st i in I holds F1.i = Funcs(X.i, Y.i) and
A2: for i be set st i in I holds F2.i = Funcs(X.i, Y.i);
    now
      let i be set;
      assume
A3:   i in I;
      hence F1.i = Funcs(X.i, Y.i) by A1
        .= F2.i by A2,A3;
    end;
    hence thesis by Th3;
  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 set st i in dom it holds it.i = (G.i)*(F.i);
  existence
  proof
    defpred P[set,set] means $2 = (G.$1)*(F.$1);
A1: for i be set st i in dom F /\ dom G ex u be set st P[i,u];
    ex H being Function st
    dom H = dom F /\ dom G & for i be set 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 set 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 set st i in dom H2 holds H2.i = (G.i)*(F.i);
    now
      let i be set;
      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,FUNCT_1:2;
  end;
end;

registration
  let F,G be Function-yielding Function;
  cluster G**F -> Function-yielding;
  coherence
  proof
    set H = G**F;
    let x be set;
    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[set,set] means $2 = (F.$1).:(A.$1);
A1: for i be set st i in I ex u be set st P[i,u];
    consider g being Function such that
A2: dom g = I & for i be set 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 set;
      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 by Th3;
  end;
end;

registration
  let I;
  cluster [[0]]I -> empty-yielding;
  coherence
  proof
    rng [[0]]I c= {{}} by FUNCOP_1:13;
    hence thesis by RELAT_1:def 15;
  end;
end;

scheme
  MSSExD { I() -> non empty set, P[set,set] }: 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 set st P[i,j]
proof
  defpred Z[set,set] means P[ $1,$2];
A2: for i being set st i in I() ex j being set st Z[i,j] by A1;
  consider f being ManySortedSet of I() such that
A3: for i being set st i in I() holds Z[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
  proof
    set x = the Element of X;
    let f be ManySortedSet of X;
    dom f = X by PARTFUN1:def 2;
    then [x,f.x] in f by FUNCT_1:def 2;
    hence thesis;
  end;
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 set;
    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 by FUNCT_1:2;
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(set) = f.$1;
A1: for e st e in I holds F(e) <> {};
   consider g being ManySortedSet of I such that
A2:  for e st e in I holds g.e in F(e) from KuratowskiFunction(A1);
    g is f-compatible
    proof let x be set;
     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,XBOOLE_1:1;
  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 by A2,RELAT_1:69
   .= 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
  for i being Element of I holds A.i = B.i;
 compatibility
 proof
   thus A = B implies for i being Element of I holds A.i = B.i;
   assume for i being Element of I holds A.i = B.i;
    then for i being set st i in I holds A.i = B.i;
   hence thesis by Th3;
  end;
end;