:: Algebraic Operation on Subsets of Many Sorted Sets
::  by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997-2019 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 XBOOLE_0, STRUCT_0, PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1,
      MSUALG_1, TARSKI, MSUALG_2, UNIALG_2, MSSUBFAM, FUNCT_1, MARGREL1,
      SUBSET_1, FINSET_1, FUNCOP_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1,
      ZFMISC_1, CARD_3, FUNCT_2, CLOSURE3, PRE_POLY, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE,
      FINSEQ_2, MSUALG_1, MSUALG_2, CARD_3, PRE_POLY, CLOSURE2, MSSUBFAM,
      MBOOLEAN;
 constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_2, PRALG_2, CLOSURE2,
      RELSET_1, FINSEQ_2, PRE_POLY;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1,
      PBOOLE, STRUCT_0, MSUALG_1, CLOSURE2, FINSEQ_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE;
 equalities PBOOLE, ORDINAL1;
 expansions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE;
 theorems FUNCT_4, FUNCT_1, TARSKI, PBOOLE, MSUALG_1, MBOOLEAN, FUNCOP_1,
      MSUALG_2, CLOSURE2, ZFMISC_1, RELAT_1, CARD_3, MSSUBFAM, FUNCT_2,
      XBOOLE_0, SETFAM_1, PARTFUN1, FINSET_1, PRE_POLY;
 schemes CLASSES1;

begin  :: Preliminaries

registration
  let S be non empty 1-sorted;
  cluster the 1-sorted of S -> non empty;
  coherence;
end;

theorem Th1:
  for I be non empty set, M, N be ManySortedSet of I holds M +* N = N
proof
  let I be non empty set, M, N be ManySortedSet of I;
  dom M = I by PARTFUN1:def 2
    .= dom N by PARTFUN1:def 2;
  hence thesis by FUNCT_4:19;
end;

theorem
  for I be set, M, N be ManySortedSet of I, F be SubsetFamily of M holds
  N in F implies meet |:F:| c=' N by CLOSURE2:21,MSSUBFAM:43;

theorem Th3:
  for S be non void non empty ManySortedSign, MA be strict
  non-empty MSAlgebra over S for F be SubsetFamily of the Sorts of MA st F c=
  SubSort MA for B be MSSubset of MA st B = meet |:F:| holds B is opers_closed
proof
  let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
  over S;
  let F be SubsetFamily of the Sorts of MA such that
A1: F c= SubSort MA;
  let B be MSSubset of MA such that
A2: B = meet |:F:|;
  per cases;
  suppose
A3: F = {};
    set Q = the Sorts of MA;
    reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA;
    set I = the carrier of S;
    FF = EmptyMS I by A3;
    then
A4: Q = B by A2,MSSUBFAM:41;
    reconsider Q as MSSubset of MA by PBOOLE:def 18;
    for o be OperSymbol of S holds Q is_closed_on o
    proof
      let o be OperSymbol of S;
A5:   (the ResultSort of S).o = the_result_sort_of o & dom the ResultSort
      of S = the carrier' of S by FUNCT_2:def 1,MSUALG_1:def 2;
      Result(o,MA) = (Q * the ResultSort of S).o by MSUALG_1:def 5
        .= Q.(the_result_sort_of o) by A5,FUNCT_1:13;
      then
A6:   rng ((Den(o,MA))|((Q#.(the_arity_of o)))) c= Q.(the_result_sort_of
      o) by RELAT_1:def 19;
      (the Arity of S).o = the_arity_of o & dom the Arity of S = the
      carrier' of S by FUNCT_2:def 1,MSUALG_1:def 1;
      then
A7:   (Q# * (the Arity of S)).o = Q#.(the_arity_of o) by FUNCT_1:13;
      (Q * the ResultSort of S).o = Q.(the_result_sort_of o) by A5,FUNCT_1:13;
      hence thesis by A7,A6;
    end;
    hence thesis by A4;
  end;
  suppose
A8: F <> {};
    set SS = S;
    let o be OperSymbol of SS;
    set i = (the_result_sort_of o);
A9: (the ResultSort of SS).o = the_result_sort_of o by MSUALG_1:def 2;
A10: dom the ResultSort of SS = the carrier' of SS by FUNCT_2:def 1;
    (the Arity of SS).o = the_arity_of o & dom the Arity of SS = the
    carrier' of SS by FUNCT_2:def 1,MSUALG_1:def 1;
    then
A11: (B# * (the Arity of SS)).o = B#.(the_arity_of o) by FUNCT_1:13;
    Result(o,MA) = ((the Sorts of MA) * the ResultSort of SS).o by
MSUALG_1:def 5
      .= (the Sorts of MA).(the_result_sort_of o) by A9,A10,FUNCT_1:13;
    then
A12: rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= (the Sorts of MA).(
    the_result_sort_of o) by RELAT_1:def 19;
A13: rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= B.(the_result_sort_of o )
    proof
      consider Q be Subset-Family of ((the Sorts of MA).i) such that
A14:  Q = |:F:|.i and
A15:  B.i = Intersect Q by A2,MSSUBFAM:def 1;
      let v be object;
      assume
A16:  v in rng ((Den(o,MA))|((B#.(the_arity_of o))));
      then consider p be object such that
A17:  p in dom ((Den(o,MA))|(B#.(the_arity_of o))) and
A18:  v = ((Den(o,MA))|(B#.(the_arity_of o))).p by FUNCT_1:def 3;
      for Y being set st Y in Q holds v in Y
      proof
A19:    |:F:|.i = { xx.i where xx is Element of Bool the Sorts of MA : xx
        in F } by A8,CLOSURE2:14;
        let Y be set;
        assume Y in Q;
        then consider xx be Element of Bool the Sorts of MA such that
A20:    Y = xx.i and
A21:    xx in F by A14,A19;
        reconsider xx as MSSubset of MA;
        xx is opers_closed by A1,A21,MSUALG_2:14;
        then xx is_closed_on o;
        then
A22:    rng ((Den(o,MA))|((xx# * the Arity of SS).o)) c= (xx * the
        ResultSort of SS).o;
        B c= xx by A2,A21,CLOSURE2:21,MSSUBFAM:43;
        then
        (Den(o,MA))|((B# * the Arity of SS).o) c= (Den(o,MA))|((xx# * the
        Arity of SS).o) by MSUALG_2:2,RELAT_1:75;
        then
A23:    dom ((Den(o,MA))|((B# * the Arity of SS).o)) c= dom ((Den(o,MA))|
        ((xx# * the Arity of SS).o)) by RELAT_1:11;
A24:    v = (Den(o,MA)).p by A17,A18,FUNCT_1:47;
        then v = ((Den(o,MA))|((xx# * the Arity of SS).o)).p by A11,A17,A23,
FUNCT_1:47;
        then
        v in rng ((Den(o,MA))|((xx# * the Arity of SS).o)) by A11,A17,A23,
FUNCT_1:def 3;
        then (Den(o,MA)).p in (xx * the ResultSort of SS).o by A22,A24;
        then (Den(o,MA)).p in xx.((the ResultSort of SS).o) by A10,FUNCT_1:13;
        then (Den(o,MA)).p in xx.i by MSUALG_1:def 2;
        hence thesis by A17,A18,A20,FUNCT_1:47;
      end;
      hence thesis by A12,A16,A15,SETFAM_1:43;
    end;
    (B * the ResultSort of SS).o = B.(the_result_sort_of o) by A9,A10,
FUNCT_1:13;
    hence thesis by A11,A13;
  end;
end;

begin :: Relationships between Subsets Families

theorem
  for A,B,C be set holds A is_coarser_than B & B is_coarser_than C
  implies A is_coarser_than C
proof
  let A,B,C be set;
  assume that
A1: A is_coarser_than B and
A2: B is_coarser_than C;
  let a be set;
  assume a in A;
  then consider b be set such that
A3: b in B and
A4: b c= a by A1;
  consider c be set such that
A5: c in C & c c= b by A2,A3;
  take c;
  thus thesis by A4,A5;
end;

Lm1: now
  let I be non empty set, M be ManySortedSet of I;
  set F = { x where x is Element of I : M.x <> {} };
  thus support M = F
  proof
    thus support M c= F
    proof
      let x be object;
A1:   dom M = I by PARTFUN1:def 2;
A2:   support M c= dom M by PRE_POLY:37;
      assume
A3:   x in support M;
      then M.x <> {} by PRE_POLY:def 7;
      hence thesis by A1,A2,A3;
    end;
    let x be object;
    assume x in F;
    then ex i being Element of I st x = i & M.i <> {};
    hence thesis by PRE_POLY:def 7;
  end;
end;

definition
  let I be non empty set, M be ManySortedSet of I;
  redefine func support M equals
  { x where x is Element of I : M.x <> {} };
  compatibility by Lm1;
end;

theorem
  for I be non empty set, M be non-empty ManySortedSet of I holds
  M = EmptyMS I +* (M|support M)
proof
  let I be non empty set, M be non-empty ManySortedSet of I;
  set MM = M|support M;
A1: I c= support M
  proof
    let v be object;
    assume
A2: v in I;
    then M.v <> {};
    hence thesis by A2;
  end;
  dom M = I by PARTFUN1:def 2;
  then MM = M by A1,RELAT_1:68;
  hence thesis by Th1;
end;

theorem
  for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds
  M1|support M1 = M2|support M2 implies M1 = M2
proof
  let I be non empty set, M1, M2 be non-empty ManySortedSet of I;
A1: dom M1 = I by PARTFUN1:def 2;
A2: dom M2 = I by PARTFUN1:def 2;
  assume
A3: M1|support M1 = M2|support M2;
  for x be object st x in I holds M1.x = M2.x
  proof
    let x be object;
A4: dom (M2|support M2) = dom M2 /\ support M2 by RELAT_1:61;
    assume
A5: x in I;
    then M1.x is non empty;
    then
A6: x in support M1 by A5;
    M2.x is non empty by A5;
    then x in support M2 by A5;
    then
A7: x in dom (M2|support M2) by A2,A5,A4,XBOOLE_0:def 4;
    dom (M1|support M1) = dom M1 /\ support M1 by RELAT_1:61;
    then x in dom (M1|support M1) by A1,A5,A6,XBOOLE_0:def 4;
    then M1.x = (M2|support M2).x by A3,FUNCT_1:47
      .= M2.x by A7,FUNCT_1:47;
    hence thesis;
  end;
  hence thesis;
end;

::$CT

theorem Th7:
  for I being non empty set, M being ManySortedSet of I, x being
Element of Bool M, i being Element of I for y being set st y in x.i ex a being
Element of Bool M st y in a.i & a is finite-yielding & support a is finite &
a c= x
proof
  let I be non empty set, M be ManySortedSet of I, x be Element of Bool M, i
  be Element of I;
  let y be set such that
A1: y in x.i;
  set N = {i} --> {y};
  set A = EmptyMS I +* N;
A2: dom N = {i} by FUNCOP_1:13;
  then
A3: i in dom N by TARSKI:def 1;
  then
A4: N.i = {y} by A2,FUNCOP_1:7;
  then
A5: A.i = {y} by A3,FUNCT_4:13;
A6: dom A = dom EmptyMS I \/ dom N by FUNCT_4:def 1
    .= I \/ {i} by A2,PARTFUN1:def 2
    .= I by ZFMISC_1:40;
  then reconsider A as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
  for j be object st j in I holds A.j c= M.j
  proof
    let j be object such that
A7: j in I;
    per cases;
    suppose
A8:   i = j;
      reconsider x as ManySortedSubset of M;
      let v be object;
      assume v in A.j;
      then v in {y} by A3,A4,A8,FUNCT_4:13;
      then
A9:   v in x.j by A1,A8,TARSKI:def 1;
      x c= M by PBOOLE:def 18;
      then x.j c= M.j by A7;
      hence thesis by A9;
    end;
    suppose
      i <> j;
      then
A10:  not j in {i} by TARSKI:def 1;
      j in dom EmptyMS I \/ dom N by A6,A7,FUNCT_4:def 1;
      then A.j = (I --> {}).j by A2,A10,FUNCT_4:def 1
        .= {} by A7,FUNCOP_1:7;
      hence thesis;
    end;
  end;
  then A c= M;
  then reconsider AA = A as ManySortedSubset of M by PBOOLE:def 18;
  reconsider a = AA as Element of Bool M by CLOSURE2:def 1;
A11: for j be object st j in I holds a.j c= x.j
  proof
    let j be object such that
A12: j in I;
    per cases;
    suppose
A13:  i = j;
      let v be object;
      assume
A14:  v in a.j;
      a.j = {y} by A3,A4,A13,FUNCT_4:13;
      hence thesis by A1,A13,A14,TARSKI:def 1;
    end;
    suppose
      j <> i;
      then
A15:  not j in {i} by TARSKI:def 1;
      j in dom EmptyMS I \/ dom N by A6,A12,FUNCT_4:def 1;
      then a.j = (I --> {}).j by A2,A15,FUNCT_4:def 1
        .= {} by A12,FUNCOP_1:7;
      hence thesis;
    end;
  end;
A16: { b where b is Element of I : a.b <> {}} = {i}
  proof
    thus { b where b is Element of I : a.b <> {}} c= {i}
    proof
      let s be object;
      assume s in { b where b is Element of I : a.b <> {}};
      then
A17:  ex b be Element of I st s = b & a.b <> {};
      assume
A18:  not s in {i};
      reconsider s as Element of I by A17;
      s in dom a by A6;
      then s in dom EmptyMS I \/ dom N by FUNCT_4:def 1;
      then a.s = (I --> {}).s by A2,A18,FUNCT_4:def 1
        .= {} by FUNCOP_1:7;
      hence contradiction by A17;
    end;
    let s be object;
    assume
A19: s in {i};
    then
A20: s = i by TARSKI:def 1;
    reconsider s as Element of I by A19,TARSKI:def 1;
    a.s = {y} by A3,A4,A20,FUNCT_4:13;
    hence thesis;
  end;
  take a;
  for j be object st j in I holds a.j is finite
  proof
    let j be object such that
A21: j in I;
    per cases;
    suppose
      j = i;
      hence thesis by A3,A4,FUNCT_4:13;
    end;
    suppose
      j <> i;
      then
A22:  not j in {i} by TARSKI:def 1;
      j in dom EmptyMS I \/ dom N by A6,A21,FUNCT_4:def 1;
      then a.j = (I --> {}).j by A2,A22,FUNCT_4:def 1
        .= {} by A21,FUNCOP_1:7;
      hence thesis;
    end;
  end;
  hence thesis by A5,A16,A11,FINSET_1:def 5,TARSKI:def 1;
end;

definition
  let I be set, M be ManySortedSet of I;
  let A be SubsetFamily of M;
  func MSUnion A -> ManySortedSubset of M means
  :Def2:
  for i be set st i in I
  holds it.i = union { f.i where f is Element of Bool M: f in A };
  existence
  proof
    defpred P[object,object] means
    $2 = union { f.$1 where f is Element of Bool M:f in A };
A1: for x be object st x in I ex y be object st P[x,y];
    consider IT be Function such that
A2: dom IT = I and
A3: for x be object st x in I holds P[x, IT.x] from CLASSES1:sch 1(A1);
    reconsider IT as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
    for i be object st i in I holds IT.i c= M.i
    proof
      let i be object such that
A4:   i in I;
      for x be object holds x in IT.i implies x in M.i
      proof
        let x be object;
        assume
A5:     x in IT.i;
        IT.i = union { f.i where f is Element of Bool M: f in A } by A3,A4;
        then consider Y be set such that
A6:     x in Y and
A7:     Y in { f.i where f is Element of Bool M: f in A } by A5,TARSKI:def 4;
        consider ff be Element of Bool M such that
A8:     ff.i = Y and
        ff in A by A7;
        reconsider ff as ManySortedSubset of M;
        ff c= M by PBOOLE:def 18;
        then ff.i c= M.i by A4;
        hence thesis by A6,A8;
      end;
      hence thesis;
    end;
    then IT c= M;
    then reconsider IT as ManySortedSubset of M by PBOOLE:def 18;
    take IT;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let B1,B2 be ManySortedSubset of M;
    assume that
A9: for i be set st i in I holds B1.i = union { f.i where f is
    Element of Bool M: f in A } and
A10: for i be set st i in I holds B2.i = union { ff.i where ff is
    Element of Bool M: ff in A };
    for i be object st i in I holds B1.i = B2.i
    proof
      let i be object;
      assume
A11:  i in I;
      then B1.i = union { f.i where f is Element of Bool M : f in A } by A9
        .= B2.i by A10,A11;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M;
  cluster MSUnion A -> empty-yielding;
  coherence
  proof
    let i be object;
    set MA = MSUnion A;
    assume i in I;
    then
A1: MA.i = union {f.i where f is Element of Bool M : f in A} by Def2;
    assume MA.i is non empty;
    then consider v being object such that
A2: v in MA.i;
    consider h be set such that
    v in h and
A3: h in {f.i where f is Element of Bool M : f in A} by A1,A2,TARSKI:def 4;
    ex g be Element of Bool M st h = g.i & g in A by A3;
    hence contradiction;
  end;
end;

theorem
  for I be set, M be ManySortedSet of I, A be SubsetFamily of M holds
  MSUnion A = union |:A:|
proof
  let I be set, M be ManySortedSet of I, A be SubsetFamily of M;
  set AA = |:A:|;
  reconsider UA = union AA as ManySortedSet of I;
  per cases;
  suppose
A1: A is non empty;
    for i be object st i in I holds (MSUnion A).i = UA.i
    proof
      let i be object;
      assume
A2:   i in I;
      then
      AA.i = { g.i where g is Element of Bool M : g in A } & UA.i = union
      (AA.i) by A1,CLOSURE2:14,MBOOLEAN:def 2;
      hence thesis by A2,Def2;
    end;
    hence thesis;
  end;
  suppose
A3: A is empty SubsetFamily of M;
    for i be object st i in I holds (MSUnion A).i = UA.i
    proof
      let i be object;
      assume i in I;
      AA = EmptyMS I by A3;
      then UA = EmptyMS I by MBOOLEAN:21;
      then UA.i is empty;
      hence thesis by A3;
    end;
    hence thesis;
  end;
end;

definition
  let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
  redefine func A \/ B -> SubsetFamily of M;
  correctness by CLOSURE2:3;
end;

theorem
  for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M
  holds MSUnion (A \/ B) = MSUnion A (\/) MSUnion B
proof
  let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
  reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M;
  reconsider MAB as ManySortedSet of I;
  reconsider MA = MSUnion A as ManySortedSubset of M;
  reconsider MA as ManySortedSet of I;
  reconsider MB = MSUnion B as ManySortedSubset of M;
  reconsider MB as ManySortedSet of I;
  for i be object st i in I holds MAB.i = (MA (\/) MB).i
  proof
    let i be object;
    assume
A1: i in I;
    then
A2: MAB.i = union {f.i where f is Element of Bool M : f in (A \/ B)} by Def2;
A3: (MA (\/) MB).i = MA.i \/ MB.i by A1,PBOOLE:def 4;
A4: for v be object holds v in (MA (\/) MB).i implies v in MAB.i
    proof
      let v be object;
      assume v in (MA (\/) MB).i;
      then
A5:   v in MA.i or v in MB.i by A3,XBOOLE_0:def 3;
      per cases by A1,A5,Def2;
      suppose
        v in union { f.i where f is Element of Bool M : f in A};
        then consider g be set such that
A6:     v in g and
A7:     g in { f.i where f is Element of Bool M : f in A} by TARSKI:def 4;
        consider h be Element of Bool M such that
A8:     g = h.i and
A9:     h in A by A7;
        h in A \/ B by A9,XBOOLE_0:def 3;
        then
        g in { f.i where f is Element of Bool M : f in (A \/ B)} by A8;
        hence thesis by A2,A6,TARSKI:def 4;
      end;
      suppose
        v in union { f.i where f is Element of Bool M : f in B};
        then consider g be set such that
A10:    v in g and
A11:    g in { f.i where f is Element of Bool M : f in B} by TARSKI:def 4;
        consider h be Element of Bool M such that
A12:    g = h.i and
A13:    h in B by A11;
        h in A \/ B by A13,XBOOLE_0:def 3;
        then
        g in { f.i where f is Element of Bool M : f in (A \/ B)} by A12;
        hence thesis by A2,A10,TARSKI:def 4;
      end;
    end;
A14: MA.i = union {f.i where f is Element of Bool M : f in A } & MB.i =
    union {f. i where f is Element of Bool M : f in B } by A1,Def2;
    for v be object holds v in MAB.i implies v in (MA (\/) MB).i
    proof
      let v be object;
      assume v in MAB.i;
      then consider h be set such that
A15:  v in h and
A16:  h in {f.i where f is Element of Bool M : f in (A \/ B)} by A2,
TARSKI:def 4;
      consider g be Element of Bool M such that
A17:  h = g.i and
A18:  g in (A \/ B) by A16;
      g in A or g in B by A18,XBOOLE_0:def 3;
      then h in {f.i where f is Element of Bool M : f in A } or h in {f.i
      where f is Element of Bool M : f in B } by A17;
      then v in union {f.i where f is Element of Bool M : f in A } or v in
      union {f.i where f is Element of Bool M : f in B } by A15,TARSKI:def 4;
      hence thesis by A3,A14,XBOOLE_0:def 3;
    end;
    hence thesis by A4,TARSKI:2;
  end;
  hence thesis;
end;

theorem
  for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M
  holds A c= B implies MSUnion A c= MSUnion B
proof
  let I be set, M be ManySortedSet of I;
  let A, B be SubsetFamily of M;
  reconsider MA = MSUnion A as ManySortedSubset of M;
  reconsider MA as ManySortedSet of I;
  reconsider MB = MSUnion B as ManySortedSubset of M;
  reconsider MB as ManySortedSet of I;
  assume
A1: A c= B;
  for i be object st i in I holds MA.i c= MB.i
  proof
    let i be object such that
A2: i in I;
    for v be object st v in MA.i holds v in MB.i
    proof
A3:   MA.i = union {f.i where f is Element of Bool M : f in A} by A2,Def2;
      let v be object;
      assume v in MA.i;
      then consider h be set such that
A4:   v in h and
A5:   h in {f.i where f is Element of Bool M : f in A} by A3,TARSKI:def 4;
      ex g be Element of Bool M st h = g.i & g in A by A5;
      then h in {k.i where k is Element of Bool M : k in B} by A1;
      then v in union {k.i where k is Element of Bool M : k in B} by A4,
TARSKI:def 4;
      hence thesis by A2,Def2;
    end;
    hence thesis;
  end;
  hence thesis;
end;

definition
  let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
  redefine func A /\ B -> SubsetFamily of M;
  correctness by CLOSURE2:4;
end;

theorem
  for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M
  holds MSUnion (A /\ B) c= MSUnion A (/\) MSUnion B
proof
  let I be set, M be ManySortedSet of I;
  let A, B be SubsetFamily of M;
  reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I;
  reconsider MA = MSUnion A as ManySortedSet of I;
  reconsider MB = MSUnion B as ManySortedSet of I;
  for i be object st i in I holds MAB.i c= (MA (/\) MB).i
  proof
    let i be object;
    assume
A1: i in I;
    then
A2: MA.i = union {f.i where f is Element of Bool M : f in A } & MB.i =
    union {f. i where f is Element of Bool M : f in B } by Def2;
A3: MAB.i = union {f.i where f is Element of Bool M : f in (A /\ B)} by A1,Def2
;
    for v be object st v in MAB.i holds v in (MA (/\) MB).i
    proof
      let v be object;
      assume v in MAB.i;
      then consider w be set such that
A4:   v in w and
A5:   w in {f.i where f is Element of Bool M : f in (A /\ B)} by A3,
TARSKI:def 4;
      consider g be Element of Bool M such that
A6:   w = g.i and
A7:   g in A /\ B by A5;
      g in B by A7,XBOOLE_0:def 4;
      then w in {f.i where f is Element of Bool M : f in B } by A6;
      then
A8:   v in union {f.i where f is Element of Bool M : f in B } by A4,
TARSKI:def 4;
      g in A by A7,XBOOLE_0:def 4;
      then w in {f.i where f is Element of Bool M : f in A } by A6;
      then v in union {f.i where f is Element of Bool M : f in A } by A4,
TARSKI:def 4;
      then v in (MA.i /\ MB.i) by A2,A8,XBOOLE_0:def 4;
      hence thesis by A1,PBOOLE:def 5;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  for I be set, M be ManySortedSet of I, AA be set st for x being set st
  x in AA holds x is SubsetFamily of M for A,B be SubsetFamily of M st B = {
MSUnion X where X is SubsetFamily of M : X in AA} & A = union AA holds MSUnion
  B = MSUnion A
proof
  let I be set, M be ManySortedSet of I, AA be set such that
A1: for x being set st x in AA holds x is SubsetFamily of M;
  let A,B be SubsetFamily of M such that
A2: B = { MSUnion X where X is SubsetFamily of M : X in AA} and
A3: A = union AA;
    let i be object such that
A4: i in I;
   thus (MSUnion B).i c= (MSUnion A).i
    proof
      let a be object;
      thus a in (MSUnion B).i implies a in (MSUnion A).i
      proof
        assume a in (MSUnion B).i;
        then a in union { f.i where f is Element of Bool M: f in B} by A4,Def2;
        then consider Y be set such that
A5:     a in Y and
A6:     Y in { f.i where f is Element of Bool M: f in B} by TARSKI:def 4;
        consider f be Element of Bool M such that
A7:     f.i = Y and
A8:     f in B by A6;
        consider Q be SubsetFamily of M such that
A9:     f = MSUnion Q and
A10:    Q in AA by A2,A8;
        (MSUnion Q).i = union { g.i where g is Element of Bool M : g in Q
        } by A4,Def2;
        then consider d be set such that
A11:    a in d and
A12:    d in { g.i where g is Element of Bool M : g in Q} by A5,A7,A9,
TARSKI:def 4;
        consider g be Element of Bool M such that
A13:    d = g.i and
A14:    g in Q by A12;
        g in union AA by A10,A14,TARSKI:def 4;
        then
        d in { h.i where h is Element of Bool M: h in union AA } by A13;
        then
        a in union { h.i where h is Element of Bool M: h in union AA } by A11,
TARSKI:def 4;
        hence thesis by A3,A4,Def2;
      end;
    end;
    let a be object;
      assume a in (MSUnion A).i;
      then a in union { f.i where f is Element of Bool M: f in A} by A4,Def2;
      then consider Y be set such that
A15:  a in Y and
A16:  Y in { f.i where f is Element of Bool M: f in A} by TARSKI:def 4;
      consider f be Element of Bool M such that
A17:  f.i = Y and
A18:  f in A by A16;
      consider c be set such that
A19:  f in c and
A20:  c in AA by A3,A18,TARSKI:def 4;
      reconsider c as SubsetFamily of M by A1,A20;
      f.i in {v.i where v is Element of Bool M: v in c} by A19;
      then
A21:  a in union {v.i where v is Element of Bool M: v in c} by A15,A17,
TARSKI:def 4;
      (MSUnion c).i = union {v.i where v is Element of Bool M: v in c} by A4
,Def2;
      then consider cos be set such that
A22:  a in cos and
A23:  cos = (MSUnion c).i by A21;
      MSUnion c in { MSUnion X where X is SubsetFamily of M : X in AA } by A20;
      then cos in { t.i where t is Element of Bool M : t in B} by A2,A23;
      then a in union { t.i where t is Element of Bool M : t in B} by A22,
TARSKI:def 4;
      hence thesis by A4,Def2;
end;

begin ::Algebraic Operation on Subsets of Many Sorted Sets

definition
  let I be non empty set, M be ManySortedSet of I, S be SetOp of M;
  attr S is algebraic means
  for x be Element of Bool M st x = S.x
  ex A be SubsetFamily of M st A = { S.a where a is Element of Bool M :
  a is finite-yielding & support a is finite & a c= x} & x = MSUnion A;
end;

registration
  let I be non empty set, M be ManySortedSet of I;
  cluster algebraic reflexive monotonic idempotent for SetOp of M;
  existence
  proof
    reconsider f = id (Bool M) as SetOp of M;
    take f;
    thus f is algebraic
    proof
      let x be Element of Bool M such that
      x = f.x;
      set A = { f.a where a is Element of Bool M : a is finite-yielding &
      support a is finite & a c= x};
      A c= Bool M
      proof
        let v be object;
        assume v in A;
        then
        ex a be Element of Bool M st v = f.a & a is finite-yielding & support
        a is finite & a c= x;
        hence thesis;
      end;
      then reconsider A as SubsetFamily of M;
      take A;
      thus A = { f.a where a is Element of Bool M : a is finite-yielding &
      support a is finite & a c= x};
        let i be Element of I;
      thus x.i c= (MSUnion A).i
       proof let y be object;
        assume y in x.i;
        then consider a be Element of Bool M such that
A1:     y in a.i and
A2:     a is finite-yielding & support a is finite & a c= x by Th7;
        a = f.a;
        then a in A by A2;
        then a.i in {g.i where g is Element of Bool M : g in A};
        then y in union {g.i where g is Element of Bool M : g in A} by A1,
TARSKI:def 4;
        hence thesis by Def2;
      end;
          let v be object;
          assume v in (MSUnion A).i;
          then
          v in union {ff.i where ff is Element of Bool M: ff in A} by Def2;
          then consider Y be set such that
A3:       v in Y and
A4:       Y in {ff.i where ff is Element of Bool M: ff in A} by TARSKI:def 4;
          consider ff be Element of Bool M such that
A5:       Y = ff.i and
A6:       ff in A by A4;
          consider a be Element of Bool M such that
A7:       ff = f.a and
          a is finite-yielding and
          support a is finite and
A8:      a c= x by A6;
          ff = a by A7;
          then ff.i c= x.i by A8;
          hence thesis by A3,A5;
    end;
    thus f is reflexive;
    thus f is monotonic;
    thus f is idempotent;
  end;
end;

definition
  let S be non empty 1-sorted, IT be ClosureSystem of S;
  attr IT is algebraic means
  ClSys->ClOp IT is algebraic;
end;

definition
  let S be non void non empty ManySortedSign, MA be non-empty MSAlgebra over S;
  func SubAlgCl MA -> strict ClosureStr over the 1-sorted of S means
  :Def5:
  the Sorts of it = the Sorts of MA & the Family of it = SubSort MA;
  existence
  proof
    reconsider SS = the Sorts of MA as ManySortedSet of the carrier of the
    1-sorted of S;
    SubSort MA c= Bool the Sorts of MA
    proof
      let x be object;
      assume x in SubSort MA;
      then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;
      hence thesis by CLOSURE2:def 1;
    end;
    then reconsider SF = SubSort MA as SubsetFamily of SS;
    take ClosureStr (#SS, SF#);
    thus thesis;
  end;
  uniqueness;
end;

theorem Th13:
  for S be non void non empty ManySortedSign, MA be strict
  non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative
  SubsetFamily of the Sorts of MA
proof
  let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
  over S;
  SubSort MA c= Bool the Sorts of MA
  proof
    let x be object;
    assume x in SubSort MA;
    then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;
    hence thesis by CLOSURE2:def 1;
  end;
  then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA;
  for F be SubsetFamily of the Sorts of MA st F c= SUBMA holds meet |:F:|
  in SUBMA
  proof
    set M = bool (Union (the Sorts of MA));
    set I = the carrier of S;
    let F be SubsetFamily of the Sorts of MA such that
A1: F c= SUBMA;
    set x = meet |:F:|;
A2: dom x = I by PARTFUN1:def 2;
    rng x c= M
    proof
      let u be object;
       reconsider uu=u as set by TARSKI:1;
      assume u in rng x;
      then consider i be object such that
A3:   i in dom x and
A4:   u = x.i by FUNCT_1:def 3;
      dom (the Sorts of MA) = I by PARTFUN1:def 2;
      then (the Sorts of MA).i in rng (the Sorts of MA) by A2,A3,FUNCT_1:def 3;
      then
A5:   (the Sorts of MA).i c= union rng (the Sorts of MA) by ZFMISC_1:74;
      ex Q be Subset-Family of (the Sorts of MA).i st Q = |:F:|. i & u =
      Intersect Q by A2,A3,A4,MSSUBFAM:def 1;
      then uu c= union rng (the Sorts of MA) by A5;
      then u in bool (union rng (the Sorts of MA));
      hence thesis by CARD_3:def 4;
    end;
    then
A6: x in Funcs ( I, M) by A2,FUNCT_2:def 2;
    reconsider x as MSSubset of MA;
    for B be MSSubset of MA st B = x holds B is opers_closed by A1,Th3;
    hence thesis by A6,MSUALG_2:def 11;
  end;
  hence thesis by CLOSURE2:def 7;
end;

registration
  let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
  over S;
  cluster SubAlgCl MA -> absolutely-multiplicative;
  coherence
  proof
    thus SubAlgCl MA is absolutely-multiplicative
    proof
      reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of
      the Sorts of MA by Th13;
      set F = the Family of SubAlgCl MA;
      the Sorts of SubAlgCl MA = the Sorts of MA & F = SF by Def5;
      hence thesis;
    end;
  end;
end;

registration
  let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
  over S;
  cluster SubAlgCl MA -> algebraic;
  coherence
  proof
    set I = the carrier of S;
    set SS = ClSys->ClOp SubAlgCl MA, M = the Sorts of SubAlgCl MA;
    let x be Element of Bool M such that
A1: x = SS.x;
    set A = { SS.a where a is Element of Bool M : a is finite-yielding &
    support a is finite & a c= x};
    A c= Bool M
    proof
      let v be object;
      assume v in A;
      then
      ex a be Element of Bool M st v = SS.a & a is finite-yielding & support a
      is finite & a c= x;
      then reconsider vv = v as Element of Bool M;
      vv in Bool M;
      hence thesis;
    end;
    then reconsider A as SubsetFamily of M;
    take A;
    thus A = { SS.b where b is Element of Bool M : b is finite-yielding &
    support b is finite & b c= x};
    reconsider y = x, z = MSUnion A as ManySortedSet of I;
    y = z
    proof
    let i be Element of I;
      reconsider SS9 = SS as reflexive SetOp of M;
      thus y.i c= z.i
      proof
      let v be object;
      assume v in y.i;
      then consider b be Element of Bool M such that
A2:   v in b.i and
A3:   b is finite-yielding & support b is finite & b c= x by Th7;
      b c=' SS9.b by CLOSURE2:def 10;
      then
A4:   b.i c= (SS9.b).i;
      SS.b in A by A3;
      then (SS9.b).i in {f.i where f is Element of Bool M : f in A};
      then v in union {f.i where f is Element of Bool M : f in A} by A2,A4,
TARSKI:def 4;
      hence thesis by Def2;
    end;
        reconsider SS9 = SS as monotonic SetOp of M;
        let v be object;
        assume v in z.i;
        then v in union {ff.i where ff is Element of Bool M: ff in A} by Def2;
        then consider Y be set such that
A5:     v in Y and
A6:     Y in {ff.i where ff is Element of Bool M: ff in A} by TARSKI:def 4;
        consider ff be Element of Bool M such that
A7:     Y = ff.i and
A8:    ff in A by A6;
        consider a be Element of Bool M such that
A9:    ff = SS.a and
        a is finite-yielding and
        support a is finite and
A10:    a c=' x by A8;
        SS9.a c=' SS9.x by A10,CLOSURE2:def 11;
        then ff.i c= x.i by A1,A9;
        hence thesis by A5,A7;
   end;
   hence thesis;
  end;
end;