The Mizar article:

Extensions of Mappings on Generator Set

by
Artur Kornilowicz

Received March 23, 1995

Copyright (c) 1995 Association of Mizar Users

MML identifier: EXTENS_1
[ MML identifier index ]


environ

 vocabulary AMI_1, MSUALG_1, ZF_REFLE, PBOOLE, PRALG_1, MSUALG_3, RELAT_1,
      BOOLE, FUNCT_1, FUNCT_6, MSUALG_2, REALSET1, NATTRA_1, MSAFREE, LANG1,
      MCART_1, TREES_4, CQC_LANG, ALG_1, GROUP_6, FREEALG, PRELAMB, UNIALG_2,
      QC_LANG1, TDGROUP, CARD_3, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, MCART_1,
      STRUCT_0, LANG1, FUNCT_2, CARD_3, FINSEQ_4, FUNCT_6, TREES_4, DTCONSTR,
      PBOOLE, CQC_LANG, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, AUTALG_1,
      MSAFREE;
 constructors CQC_LANG, MSUALG_3, AUTALG_1, MSAFREE, FINSEQ_4, MEMBERED,
      XBOOLE_0;
 clusters FUNCT_1, MSAFREE, MSUALG_1, MSUALG_2, MSUALG_3, PBOOLE, PRALG_1,
      RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions MSUALG_1, MSUALG_2, MSUALG_3, PBOOLE, PRALG_1, TARSKI, XBOOLE_0;
 theorems AUTALG_1, CQC_LANG, FUNCT_1, FUNCT_2, FUNCT_6, MCART_1, MSAFREE,
      MSAFREE2, MSUALG_1, MSUALG_2, MSUALG_3, MSUHOM_1, PBOOLE, RELAT_1,
      CARD_3, FINSEQ_4, RELSET_1;
 schemes FUNCT_2, MSAFREE1, MSUALG_1, PBOOLE;

begin :: Preliminaries

reserve S for non void non empty ManySortedSign,
        U1, U2, U3 for non-empty MSAlgebra over S,
        I for set,
        A for ManySortedSet of I,
        B, C for non-empty ManySortedSet of I;

Lm1:
for I be set for A, B, C be ManySortedSet of I
 for F be ManySortedFunction of A, B
  for G be ManySortedFunction of B, C
 holds G ** F is ManySortedSet of I
  proof
    let I be set;
    let A, B, C be ManySortedSet of I;
    let F be ManySortedFunction of A, B;
    let G be ManySortedFunction of B, C;
      dom (G ** F) = (dom F) /\ (dom G) by MSUALG_3:def 4
                .= I /\ (dom G) by PBOOLE:def 3
                .= I /\ I by PBOOLE:def 3
                .= I;
    hence thesis by PBOOLE:def 3;
  end;

theorem Th1:
for R be Relation, X, Y be set st X c= Y holds (R|Y).:X = R.:X
  proof
   let R be Relation,
       X, Y be set such that
A1: X c= Y;
   thus (R|Y).:X c= R.:X by RELAT_1:161;
   let y be set;
   assume y in R.:X;
   then consider x1 be set such that
A2: [x1,y] in R and
A3: x1 in X by RELAT_1:def 13;
     ex x be set st [x,y] in R|Y & x in X
   proof
    take x = x1;
    thus [x,y] in R|Y by A1,A2,A3,RELAT_1:def 11;
    thus thesis by A3;
   end;
   hence y in (R|Y).:X by RELAT_1:def 13;
  end;

canceled;

theorem Th3:
for f be Function-yielding Function holds dom doms f = dom f
  proof
   let f be Function-yielding Function;
   thus dom doms f c= dom f
   proof
    let i be set;
      dom doms f = f"SubFuncs rng f by FUNCT_6:def 2;
    hence i in dom doms f implies i in dom f by FUNCT_6:28;
   end;
   thus dom f c= dom doms f
   proof
    let i be set; assume
A1:  i in dom f;
A2: f.i is Function;
      dom doms f = f"SubFuncs rng f by FUNCT_6:def 2;
    hence i in dom doms f by A1,A2,FUNCT_6:28;
   end;
  end;

theorem Th4:
for f be Function-yielding Function holds dom rngs f = dom f
  proof
   let f be Function-yielding Function;
   thus dom rngs f c= dom f
   proof
    let i be set;
      dom rngs f = f"SubFuncs rng f by FUNCT_6:def 3;
    hence i in dom rngs f implies i in dom f by FUNCT_6:28;
   end;
   thus dom f c= dom rngs f
   proof
    let i be set; assume
A1:  i in dom f;
A2: f.i is Function;
      dom rngs f = f"SubFuncs rng f by FUNCT_6:def 3;
    hence i in dom rngs f by A1,A2,FUNCT_6:28;
   end;
  end;

begin :: Facts about Many Sorted Functions

theorem
  for F be ManySortedFunction of A, B
 for X be ManySortedSubset of A st A c= X
  holds F || X = F
  proof
   let F be ManySortedFunction of A, B,
       X be ManySortedSubset of A such that
A1: A c= X;
     now
    let i be set; assume
A2:  i in I;
    then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
A3: A.i c= X.i by A1,A2,PBOOLE:def 5;
    thus (F || X).i = (f | (X.i)) by A2,MSAFREE:def 1
                   .= F.i by A3,FUNCT_2:40;
   end;
   hence thesis by PBOOLE:3;
  end;

theorem
  for A, B be ManySortedSet of I
 for M be ManySortedSubset of A
  for F be ManySortedFunction of A, B
 holds F.:.:M c= F.:.:A
  proof
   let A, B be ManySortedSet of I,
       M be ManySortedSubset of A,
       F be ManySortedFunction of A, B;
   let i be set such that
A1: i in I;
   let x be set such that
A2: x in (F.:.:M).i;
   reconsider f = F.i as Function of A.i, B.i by A1,MSUALG_1:def 2;
A3:(F.:.:M).i = f.:(M.i) by A1,MSUALG_3:def 6;
     M c= A by MSUALG_2:def 1;
   then M.i c= A.i by A1,PBOOLE:def 5;
   then f.:(M.i) c= f.:(A.i) by RELAT_1:156;
   then x in f.:(A.i) by A2,A3;
   hence x in (F.:.:A).i by A1,MSUALG_3:def 6;
  end;

theorem
  for F be ManySortedFunction of A, B
 for M1, M2 be ManySortedSubset of A st M1 c= M2
  holds (F||M2).:.:M1 = F.:.:M1
  proof
   let F be ManySortedFunction of A, B,
       M1, M2 be ManySortedSubset of A such that
A1: M1 c= M2;
     now
    let i be set; assume
A2:  i in I;
    then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
    reconsider fm = (F||M2).i as Function of M2.i, B.i by A2,MSUALG_1:def 2;
A3: M1.i c= M2.i by A1,A2,PBOOLE:def 5;
      fm = f|(M2.i) by A2,MSAFREE:def 1;
    hence ((F||M2).:.:M1).i = (f|(M2.i)).:(M1.i) by A2,MSUALG_3:def 6
                         .= f.:(M1.i) by A3,Th1
                         .= (F.:.:M1).i by A2,MSUALG_3:def 6;
   end;
   hence (F||M2).:.:M1 = F.:.:M1 by PBOOLE:3;
  end;

theorem Th8:
for F be ManySortedFunction of A, B
 for G be ManySortedFunction of B, C
  for X be ManySortedSubset of A
 holds (G ** F) || X = G ** (F || X)
  proof
   let F be ManySortedFunction of A, B,
       G be ManySortedFunction of B, C,
       X be ManySortedSubset of A;
     now
    let i be set; assume
A1:  i in I;
    then reconsider gf = (G ** F).i as Function of A.i, C.i by MSUALG_1:def 2;
    reconsider f = F.i as Function of A.i, B.i by A1,MSUALG_1:def 2;
    reconsider g = G.i as Function of B.i, C.i by A1,MSUALG_1:def 2;
    reconsider fx = (F || X).i as Function of X.i, B.i by A1,MSUALG_1:def 2;
    thus ((G ** F) || X).i = gf | (X.i) by A1,MSAFREE:def 1
                          .= (g*f) | (X.i) by A1,MSUALG_3:2
                          .= g * (f | (X.i)) by RELAT_1:112
                          .= g * fx by A1,MSAFREE:def 1
                          .= (G ** (F || X)).i by A1,MSUALG_3:2;
   end;
   hence thesis by PBOOLE:3;
  end;

theorem
  for A, B be ManySortedSet of I st A is_transformable_to B
 for F be ManySortedFunction of A, B
  for C be ManySortedSet of I st B is ManySortedSubset of C
 holds F is ManySortedFunction of A, C
  proof
   let A, B be ManySortedSet of I such that
A1: A is_transformable_to B;
   let F be ManySortedFunction of A, B,
       C be ManySortedSet of I such that
A2: B is ManySortedSubset of C;
   let i be set such that
A3: i in I;
     B c= C by A2,MSUALG_2:def 1;
then A4:(B.i) c= (C.i) by A3,PBOOLE:def 5;
A5:B.i = {} implies A.i = {} by A1,A3,AUTALG_1:def 4;
     F.i is Function of A.i, B.i by A3,MSUALG_1:def 2;
   hence F.i is Function of A.i, C.i by A4,A5,FUNCT_2:9;
  end;

theorem
  for F be ManySortedFunction of A, B
 for X be ManySortedSubset of A
  holds F is "1-1" implies F || X is "1-1"
  proof
   let F be ManySortedFunction of A, B,
       X be ManySortedSubset of A;
   assume
A1: F is "1-1";
     now
    let i be set; assume
A2:  i in I;
    then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
      f is one-to-one by A1,A2,MSUALG_3:1;
    then f | (X.i) is one-to-one by FUNCT_1:84;
    hence (F||X).i is one-to-one by A2,MSAFREE:def 1;
   end;
   hence thesis by MSUALG_3:1;
  end;

begin :: doms & rngs of Many Sorted Function

definition let I; let F be ManySortedFunction of I;
 redefine func doms F -> ManySortedSet of I;
coherence
  proof
     dom doms F = dom F by Th3
             .= I by PBOOLE:def 3;
   hence doms F is ManySortedSet of I by PBOOLE:def 3;
  end;
 redefine func rngs F -> ManySortedSet of I;
coherence
  proof
     dom rngs F = dom F by Th4
             .= I by PBOOLE:def 3;
   hence rngs F is ManySortedSet of I by PBOOLE:def 3;
  end;
end;

theorem
  for F be ManySortedFunction of A, B
 for X be ManySortedSubset of A
  holds doms (F || X) c= doms F
  proof
   let F be ManySortedFunction of A, B,
       X be ManySortedSubset of A;
   let i be set; assume
A1: i in I;
   then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
     dom F = I by PBOOLE:def 3;
then A2:(doms F).i = dom f by A1,FUNCT_6:31;
A3:(F||X).i = f|(X.i) by A1,MSAFREE:def 1;
     dom (F||X) = I by PBOOLE:def 3;
   then (doms (F||X)).i = dom (f|(X.i)) by A1,A3,FUNCT_6:31;
   hence (doms (F||X)).i c= (doms F).i by A2,FUNCT_1:76;
  end;

theorem
  for F be ManySortedFunction of A, B
 for X be ManySortedSubset of A
  holds rngs (F || X) c= rngs F
  proof
   let F be ManySortedFunction of A, B,
       X be ManySortedSubset of A;
   let i be set; assume
A1: i in I;
   then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
     dom F = I by PBOOLE:def 3;
then A2:(rngs F).i = rng f by A1,FUNCT_6:31;
A3:(F||X).i = f|(X.i) by A1,MSAFREE:def 1;
     dom (F||X) = I by PBOOLE:def 3;
   then (rngs (F||X)).i = rng (f|(X.i)) by A1,A3,FUNCT_6:31;
   hence (rngs (F||X)).i c= (rngs F).i by A2,FUNCT_1:76;
  end;

theorem
  for A, B be ManySortedSet of I
 for F be ManySortedFunction of A, B
  holds F is "onto" iff rngs F = B
  proof
   let A, B be ManySortedSet of I,
       F be ManySortedFunction of A, B;
A1:dom F = I by PBOOLE:def 3;
   thus F is "onto" implies rngs F = B
   proof assume
A2:  F is "onto";
      now
     let i be set; assume
A3:   i in I;
     then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
       rng f = B.i by A2,A3,MSUALG_3:def 3;
     hence (rngs F).i = B.i by A1,A3,FUNCT_6:31;
    end;
    hence thesis by PBOOLE:3;
   end;
   assume
A4: rngs F = B;
   let i be set;
   assume i in I;
   hence rng (F.i) = B.i by A1,A4,FUNCT_6:31;
  end;

theorem
  for X be non-empty ManySortedSet of the carrier of S
 holds rngs Reverse X = X
  proof
   let X be non-empty ManySortedSet of the carrier of S;
   set I = the carrier of S,
       R = Reverse X;
     now
    let i be set such that
A1:  i in I;
A2: dom R = I by PBOOLE:def 3;
    reconsider r = R.i as Function of (FreeGen X).i, X.i by A1,MSUALG_1:def 2;
    thus (rngs R).i = X.i
    proof
     thus (rngs R).i c= X.i
     proof
      let x be set;
      assume x in (rngs R).i;
then A3:   x in rng r by A1,A2,FUNCT_6:31;
        rng r c= X.i by RELSET_1:12;
      hence x in X.i by A3;
     end;
     let x be set such that
A4:   x in X.i;
     reconsider s0 = i as SortSymbol of S by A1;
     set D = DTConMSA X;
A5:  [x,s0] in Terminals D by A4,MSAFREE:7;
     then reconsider t = [x,s0] as Symbol of D;
A6:  R.s0 = Reverse(s0, X) by MSAFREE:def 20;
then A7:  dom (R.s0) = FreeGen(s0, X) by FUNCT_2:def 1;
       t`2 = s0 by MCART_1:7;
     then root-tree t in {root-tree tt where tt is Symbol of D :
                             tt in Terminals D & tt`2 = s0} by A5;
then A8:  root-tree t in FreeGen(s0, X) by MSAFREE:14;
then A9:  (R.s0).(root-tree t) in rng (R.s0) by A7,FUNCT_1:def 5;
       (R.s0).(root-tree t) = t`1 by A6,A8,MSAFREE:def 19
                         .= x by MCART_1:7;
     hence x in (rngs R).i by A2,A9,FUNCT_6:31;
    end;
   end;
   hence thesis by PBOOLE:3;
  end;

theorem
  for F be ManySortedFunction of A, B
 for G be ManySortedFunction of B, C
  for X be non-empty ManySortedSubset of B st rngs F c= X
 holds (G || X) ** F = G ** F
  proof
   let F be ManySortedFunction of A, B,
       G be ManySortedFunction of B, C,
       X be non-empty ManySortedSubset of B such that
A1: rngs F c= X;
A2:dom F = I by PBOOLE:def 3;
A3:F is ManySortedFunction of A, X
   proof
    let i be set; assume
A4:  i in I;
    then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
A5: X.i <> {} by A4,PBOOLE:def 16;
      B.i <> {} by A4,PBOOLE:def 16;
then A6: dom f = A.i by FUNCT_2:def 1;
      (rngs F).i = rng f & (rngs F).i c= X.i
      by A1,A2,A4,FUNCT_6:31,PBOOLE:def 5;
    hence F.i is Function of A.i, X.i by A5,A6,FUNCT_2:def 1,RELSET_1:11;
   end;
then A7:(G || X) ** F is ManySortedSet of I by Lm1;
     now
    let i be set;
    assume
A8:  i in I;
then A9: X.i <> {} by PBOOLE:def 16;
    reconsider f = F.i as Function of A.i, B.i by A8,MSUALG_1:def 2;
A10: (rngs F).i = rng f & (rngs F).i c= X.i
      by A1,A2,A8,FUNCT_6:31,PBOOLE:def 5;
      B.i <> {} by A8,PBOOLE:def 16;
    then rng f c= X.i & dom f = A.i by A10,FUNCT_2:def 1;
    then reconsider f' = f as Function of A.i, X.i by A9,FUNCT_2:def 1,RELSET_1
:11;
    reconsider g = G.i as Function of B.i, C.i by A8,MSUALG_1:def 2;
    reconsider gx = (G || X).i as Function of X.i, C.i by A8,MSUALG_1:def 2;
A11: rng f' c= X.i by RELSET_1:12;
    thus ((G || X) ** F).i = gx * f' by A3,A8,MSUALG_3:2
      .= (g | (X.i)) * f by A8,MSAFREE:def 1
      .= g * f' by A11,MSUHOM_1:1
      .= (G ** F).i by A8,MSUALG_3:2;
   end;
   hence thesis by A7,PBOOLE:3;
  end;

begin :: Other properties of "onto" & "1-1"

theorem Th16:
for F be ManySortedFunction of A, B
 holds F is "onto" iff
  for C for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H
  proof
   let F be ManySortedFunction of A, B;
   thus F is "onto" implies
    for C for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H
     proof assume
A1:    F is "onto";
      let C;
      let G, H be ManySortedFunction of B, C such that
A2:    G**F = H**F;
        now
       let i be set; assume
A3:     i in I;
then A4:    B.i <> {} & C.i <> {} by PBOOLE:def 16;
       reconsider f = F.i as Function of A.i, B.i by A3,MSUALG_1:def 2;
       reconsider g = G.i as Function of B.i, C.i by A3,MSUALG_1:def 2;
       reconsider h = H.i as Function of B.i, C.i by A3,MSUALG_1:def 2;
A5:    rng f = B.i by A1,A3,MSUALG_3:def 3;
         g*f = (H**F).i by A2,A3,MSUALG_3:2
          .= h*f by A3,MSUALG_3:2;
       hence G.i = H.i by A4,A5,FUNCT_2:22;
      end;
      hence G = H by PBOOLE:3;
     end;
   assume that
A6:for C for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H and
A7: not F is "onto";
   consider j be set such that
A8: j in I & rng (F.j) <> B.j by A7,MSUALG_3:def 3;
   reconsider I as non empty set by A8;
   reconsider j as Element of I by A8;
   reconsider A,B as ManySortedSet of I;
   reconsider F as ManySortedFunction of A,B;
   reconsider f =F.j as Function of A.j,B.j;
     B.j <> {} by PBOOLE:def 16;
   then consider Z be set such that
A9: Z <> {} & ex g, h be Function of B.j, Z st g*f = h*f & g <> h
     by A8,FUNCT_2:22;
   consider g, h be Function of B.j, Z such that
A10: g*(F.j) = h*(F.j) & g <> h by A9;
     ex C be ManySortedSet of I st C is non-empty &
    ex G, H be ManySortedFunction of B, C
     st G**F = H**F & G <> H
   proof
    deffunc F(set) = IFEQ($1, j, Z, B.$1);
    consider C be ManySortedSet of I such that
A11:  for i be set st i in I holds C.i = F(i) from MSSLambda;
    take C;
    deffunc F(set) = IFEQ($1, j, g, (id B).$1);
    consider G be ManySortedSet of I such that
A12:  for i be set st i in I holds G.i = F(i) from MSSLambda;
    deffunc F(set) = IFEQ($1, j, h, (id B).$1);
    consider H be ManySortedSet of I such that
A13:  for i be set st i in I holds H.i = F(i) from MSSLambda;
    thus
    C is non-empty
    proof
     let i be set such that
A14:   i in I;
       now per cases;
      case i = j;
      then IFEQ(i, j, Z, B.i) = Z by CQC_LANG:def 1;
      hence C.i is non empty by A9,A11,A14;
      case i <> j;
then A15:   IFEQ(i, j, Z, B.i) = B.i by CQC_LANG:def 1;
        B.i <> {} by A14,PBOOLE:def 16;
      hence C.i is non empty by A11,A14,A15;
     end;
     hence C.i is non empty;
    end;
      now
     let G be ManySortedSet of I;
     let g, h be Function of B.j, Z such that g*(F.j) = h*(F.j) & g <> h and
A16:   for i be set st i in I holds G.i = IFEQ(i, j, g, (id B).i);
     thus G is Function-yielding
     proof
      let i be set;
      assume i in dom G;
then A17:   i in I by PBOOLE:def 3;
        now per cases;
       case i = j;
       then IFEQ(i, j, g, (id B).i) = g by CQC_LANG:def 1;
       hence G.i is Function by A16,A17;
       case i <> j;
       then IFEQ(i, j, g, (id B).i) = (id B).i by CQC_LANG:def 1;
hence G.i is Function by A16,A17;
      end;
      hence G.i is Function;
     end;
    end;
    then reconsider G, H as ManySortedFunction of I by A10,A12,A13;
      now
     let G be ManySortedFunction of I;
     let g, h be Function of B.j, Z such that g*(F.j) = h*(F.j) & g <> h and
A18:   for i be set st i in I holds G.i = IFEQ(i, j, g, (id B).i);
     thus G is ManySortedFunction of B, C
     proof
      let i be set such that
A19:    i in I;
        now per cases;
       case
A20:     i = j;
       then A21: IFEQ(i, j, g, (id B).i) = g by CQC_LANG:def 1;
A22:    C.i = IFEQ(i, j, Z, B.i) by A11,A20;
         IFEQ(i, j, Z, B.i) = Z by A20,CQC_LANG:def 1;
       hence G.i is Function of B.i, C.i by A18,A20,A21,A22;
       case
A23:     i <> j;
       then IFEQ(i, j, g, (id B).i) = (id B).i by CQC_LANG:def 1;
then A24:    G.i = (id B).i by A18,A19;
         IFEQ(i, j, Z, B.i) = B.i by A23,CQC_LANG:def 1;
       then B.i = C.i by A11,A19;
       hence G.i is Function of B.i, C.i by A19,A24,MSUALG_1:def 2;
      end;
      hence G.i is Function of B.i, C.i;
     end;
    end;
    then reconsider G, H as ManySortedFunction of B, C by A10,A12,A13;
    take G, H;
A25: G**F is ManySortedSet of I & H**F is ManySortedSet of I by Lm1;
      now
     let i be set such that
A26:   i in I;
       now per cases;
      case
A27:    i = j;
      then IFEQ(i, j, g, (id B).i) = g by CQC_LANG:def 1;
then A28:   g = G.i by A12,A26;
        IFEQ(i, j, h, (id B).i) = h by A27,CQC_LANG:def 1;
then A29:   h = H.i by A13,A26;
      thus (G**F).i = h*(F.j) by A10,A27,A28,MSUALG_3:2
        .= (H**F).i by A27,A29,MSUALG_3:2;
      case
A30:    i <> j;
then A31:   IFEQ(i, j, g, (id B).i) = (id B).i by CQC_LANG:def 1;
A32:   IFEQ(i, j, h, (id B).i) = (id B).i by A30,CQC_LANG:def 1;
      reconsider f' = F.i as Function of A.i, B.i by A26,MSUALG_1:def 2;
      reconsider g' = G.i as Function of B.i, C.i by A26,MSUALG_1:def 2;
      reconsider h' = H.i as Function of B.i, C.i by A26,MSUALG_1:def 2;
    g' = (id B).i by A12,A26,A31
        .= h' by A13,A26,A32;
      hence (G**F).i = h'*f' by A26,MSUALG_3:2
                   .= (H**F).i by A26,MSUALG_3:2;
     end;
     hence (G**F).i = (H**F).i;
    end;
    hence G**F = H**F by A25,PBOOLE:3;
      ex i be set st i in I & G.i <> H.i
    proof
     take i = j;
     thus i in I;
A33:  g = IFEQ(i, j, g, (id B).i) by CQC_LANG:def 1
      .= G.i by A12;
       h = IFEQ(i, j, h, (id B).i) by CQC_LANG:def 1
      .= H.i by A13;
     hence thesis by A10,A33;
    end;
    hence G <> H;
   end;
   hence contradiction by A6;
  end;

theorem Th17:
for F be ManySortedFunction of A, B st A is non-empty & B is non-empty
 holds F is "1-1" iff
  for C be ManySortedSet of I
   for G, H be ManySortedFunction of C, A st F**G = F**H holds G = H
  proof
   let F be ManySortedFunction of A, B such that
A1: A is non-empty & B is non-empty;
   thus F is "1-1" implies
    for C be ManySortedSet of I
     for G, H be ManySortedFunction of C, A st F**G = F**H holds G = H
   proof assume
A2: F is "1-1";
    let C be ManySortedSet of I;
    let G, H be ManySortedFunction of C, A such that
A3:  F**G = F**H;
      now
     let i be set; assume
A4:   i in I;
then A5:  A.i <> {} & B.i <> {} by A1,PBOOLE:def 16;
     reconsider f = F.i as Function of A.i, B.i by A4,MSUALG_1:def 2;
     reconsider g = G.i as Function of C.i, A.i by A4,MSUALG_1:def 2;
     reconsider h = H.i as Function of C.i, A.i by A4,MSUALG_1:def 2;
A6:  f is one-to-one by A2,A4,MSUALG_3:1;
       f*g = (F**H).i by A3,A4,MSUALG_3:2
        .= f*h by A4,MSUALG_3:2;
     hence G.i = H.i by A5,A6,FUNCT_2:27;
    end;
    hence G = H by PBOOLE:3;
   end;
   assume that
A7: (for C be ManySortedSet of I for G, H be ManySortedFunction of C, A st
     F**G = F**H holds G = H)
     and
A8:   not F is "1-1";
   consider j be set such that
A9: j in I & not (F.j) is one-to-one by A8,MSUALG_3:1;
A10:A.j <> {} & B.j <> {} by A1,A9,PBOOLE:def 16;
  F.j is Function of A.j, B.j by A9,MSUALG_1:def 2;
   then consider Z be set such that
A11: ex g, h be Function of Z, A.j st (F.j)*g = (F.j)*h & g <> h
     by A9,A10,FUNCT_2:27;
   consider g, h be Function of Z, A.j such that
A12: (F.j)*g = (F.j)*h & g <> h by A11;
     ex C be ManySortedSet of I st ex G, H be ManySortedFunction of C, A st
    F**G = F**H & G <> H
   proof
    deffunc F(set) = IFEQ($1, j, Z, A.$1);
    consider C be ManySortedSet of I such that
A13:  for i be set st i in I holds C.i = F(i) from MSSLambda;
    take C;
    deffunc F(set) = IFEQ($1, j, g, (id C).$1);
    consider G be ManySortedSet of I such that
A14:  for i be set st i in I holds G.i = F(i) from MSSLambda;
    deffunc F(set) = IFEQ($1, j, h, (id C).$1);
    consider H be ManySortedSet of I such that
A15:  for i be set st i in I holds H.i = F(i) from MSSLambda;
      now
     let G be ManySortedSet of I;
     let g, h be Function of Z, A.j such that (F.j)*g = (F.j)*h & g <> h and
A16:   for i be set st i in I holds G.i = IFEQ(i, j, g, (id C).i);
     thus G is Function-yielding
     proof
      let i be set;
      assume i in dom G;
then A17:    i in I by PBOOLE:def 3;
        now per cases;
       case i = j;
       then IFEQ(i, j, g, (id C).i) = g by CQC_LANG:def 1;
       hence G.i is Function by A16,A17;
       case i <> j;
       then IFEQ(i, j, g, (id C).i) = (id C).i by CQC_LANG:def 1;
hence G.i is Function by A16,A17;
      end;
      hence G.i is Function;
     end;
    end;
    then reconsider G, H as ManySortedFunction of I by A12,A14,A15;
      now
     let G be ManySortedFunction of I;
     let g, h be Function of Z, A.j such that (F.j)*g = (F.j)*h & g <> h and
A18:   for i be set st i in I holds G.i = IFEQ(i, j, g, (id C).i);
     thus G is ManySortedFunction of C, A
     proof
      let i be set such that
A19:    i in I;
        now per cases;
       case
A20:     i = j;
       then A21: IFEQ(i, j, g, (id C).i) = g by CQC_LANG:def 1;
A22:    C.i = IFEQ(i, j, Z, A.i) by A13,A19;
         IFEQ(i, j, Z, A.i) = Z by A20,CQC_LANG:def 1;
       hence G.i is Function of C.i, A.i by A18,A19,A20,A21,A22;
       case
A23:     i <> j;
       then IFEQ(i, j, g, (id C).i) = (id C).i by CQC_LANG:def 1;
then A24:    G.i = (id C).i by A18,A19;
         IFEQ(i, j, Z, A.i) = A.i by A23,CQC_LANG:def 1;
       then C.i = A.i by A13,A19;
       hence G.i is Function of C.i, A.i by A19,A24,MSUALG_1:def 2;
      end;
      hence G.i is Function of C.i, A.i;
     end;
    end;
    then reconsider G, H as ManySortedFunction of C, A by A12,A14,A15;
    take G, H;
A25: F**G is ManySortedSet of I & F**H is ManySortedSet of I by Lm1;
      now
     let i be set such that
A26:   i in I;
       now per cases;
      case
A27:    i = j;
      then IFEQ(i, j, g, (id C).i) = g by CQC_LANG:def 1;
then A28:   g = G.i by A14,A26;
        IFEQ(i, j, h, (id C).i) = h by A27,CQC_LANG:def 1;
then A29:   h = H.i by A15,A26;
      thus (F**G).i = (F.j)*h by A9,A12,A27,A28,MSUALG_3:2
        .= (F**H).i by A9,A27,A29,MSUALG_3:2;
      case
A30:    i <> j;
then A31:   IFEQ(i, j, g, (id C).i) = (id C).i by CQC_LANG:def 1;
A32:   IFEQ(i, j, h, (id C).i) = (id C).i by A30,CQC_LANG:def 1;
      reconsider f' = F.i as Function of A.i, B.i by A26,MSUALG_1:def 2;
      reconsider g' = G.i as Function of C.i, A.i by A26,MSUALG_1:def 2;
      reconsider h' = H.i as Function of C.i, A.i by A26,MSUALG_1:def 2;
    g' = (id C).i by A14,A26,A31
        .= h' by A15,A26,A32;
      hence (F**G).i = f'*h' by A26,MSUALG_3:2
                   .= (F**H).i by A26,MSUALG_3:2;
     end;
     hence (F**G).i = (F**H).i;
    end;
    hence F**G = F**H by A25,PBOOLE:3;
      ex i be set st i in I & G.i <> H.i
    proof
     take i = j;
     thus i in I by A9;
A33:  g = IFEQ(i, j, g, (id C).i) by CQC_LANG:def 1
      .= G.i by A9,A14;
       h = IFEQ(i, j, h, (id C).i) by CQC_LANG:def 1
      .= H.i by A9,A15;
     hence thesis by A12,A33;
    end;
    hence G <> H;
   end;
   hence contradiction by A7;
  end;

begin :: Extensions of Mappings on Generator Set

theorem Th18:
for X be non-empty ManySortedSet of the carrier of S
 for h1, h2 be ManySortedFunction of FreeMSA X, U1 st
  h1 is_homomorphism FreeMSA X, U1 &
   h2 is_homomorphism FreeMSA X, U1 &
    h1 || FreeGen (X) = h2 || FreeGen (X)
 holds h1 = h2
  proof
   let X be non-empty ManySortedSet of the carrier of S,
       h1, h2 be ManySortedFunction of FreeMSA X, U1;
   assume that
A1: h1 is_homomorphism FreeMSA X, U1 and
A2: h2 is_homomorphism FreeMSA X, U1 and
A3: h1 || FreeGen (X) = h2 || FreeGen (X);
A4: h1 is_homomorphism FreeMSA X, U1 by A1;
    defpred P[SortSymbol of S,set,set] means h1.$1.$3 = $2;
A5: for s be SortSymbol of S, x, y be set st y in FreeGen(s,X)
    holds h1.s.y = x iff P[s,x,y];
A6: h2 is_homomorphism FreeMSA X, U1 by A2;
A7: for s be SortSymbol of S, x, y be set st y in FreeGen(s,X)
    holds h2.s.y = x iff P[s,x,y]
    proof
     let s be SortSymbol of S,
         x, y be set such that
A8:   y in FreeGen(s, X);
     set FG = FreeGen X;
A9:  (h1 || FG).s = (h1.s) | (FG.s) &
      (h2 || FG).s = (h2.s) | (FG.s) by MSAFREE:def 1;
    y in FG.s by A8,MSAFREE:def 18;
     then ((h1.s) | (FG.s)).y = h1.s.y & ((h2.s) | (FG.s)).y = h2.s.y
      by FUNCT_1:72;
     hence thesis by A3,A9;
    end;
   thus h1 = h2 from ExtFreeGen (A4, A5, A6, A7);
  end;

theorem
  for F be ManySortedFunction of U1, U2 st F is_homomorphism U1, U2
 holds F is_epimorphism U1, U2 implies
  for U3 be non-empty MSAlgebra over S
   for h1, h2 be ManySortedFunction of U2, U3 st
    h1 is_homomorphism U2, U3 & h2 is_homomorphism U2, U3
     holds (h1**F = h2**F implies h1 = h2)
  proof
   let F be ManySortedFunction of U1, U2 such that F is_homomorphism U1, U2;
   assume
A1: F is_epimorphism U1, U2;
   let U3 be non-empty MSAlgebra over S,
       h1, h2 be ManySortedFunction of U2, U3 such that
      h1 is_homomorphism U2, U3 & h2 is_homomorphism U2, U3;
   assume
A2: h1**F = h2**F;
     F is "onto" by A1,MSUALG_3:def 10;
   hence h1 = h2 by A2,Th16;
  end;

theorem
  for F be ManySortedFunction of U2, U3 st F is_homomorphism U2, U3
 holds F is_monomorphism U2, U3 iff
  for U1 be non-empty MSAlgebra over S
   for h1, h2 be ManySortedFunction of U1, U2 st
    h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2
     holds (F**h1 = F**h2 implies h1 = h2)
  proof
   let F be ManySortedFunction of U2, U3 such that
A1: F is_homomorphism U2, U3;
   thus F is_monomorphism U2, U3 implies
    for U1 be non-empty MSAlgebra over S
     for h1, h2 be ManySortedFunction of U1, U2 st
      h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2
       holds (F**h1 = F**h2 implies h1 = h2)
   proof
    assume F is_monomorphism U2, U3;
    then F is "1-1" by MSUALG_3:def 11;
    hence thesis by Th17;
   end;
   assume that
A2: for U1 be non-empty MSAlgebra over S
     for h1, h2 be ManySortedFunction of U1, U2 st
      h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2
       holds F**h1 = F**h2 implies h1 = h2 and
A3: not F is_monomorphism U2, U3;
   set I = the carrier of S;
     not F is "1-1" by A1,A3,MSUALG_3:def 11;
   then consider j be set such that
A4: j in I & not F.j is one-to-one by MSUALG_3:1;
   set B = the Sorts of U2;
   set C = the Sorts of U3;
A5:F.j is Function of B.j, C.j by A4,MSUALG_1:def 2;
   set f = F.j;
     B.j <> {} & C.j <> {} by A4,PBOOLE:def 16;
   then consider x1, x2 be set such that
A6: x1 in B.j & x2 in B.j & f.x1 = f.x2 & x1 <> x2 by A4,A5,FUNCT_2:25;
     ex U1 be non-empty MSAlgebra over S st
    ex h1, h2 be ManySortedFunction of the Sorts of U1, the Sorts of U2
     st h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 &
      F**h1 = F**h2 & h1 <> h2
   proof
    take U1 = FreeMSA the Sorts of U2;
    reconsider FG = FreeGen(B) as GeneratorSet of U1;
A7: FG is free by MSAFREE:17;
    set r = Reverse(B);
      FG is non-empty by MSAFREE:15;
    then reconsider FGj = FG.j, Bj = B.j as non empty set by A4,PBOOLE:def 16;
    reconsider x1' = x1, x2' = x2 as Element of Bj by A6;
    deffunc F(set) = x1';
    deffunc G(set) = x2';
    consider g be Function of FGj, Bj such that
A8:  for x be Element of FGj holds g.x = F(x) from LambdaD;
    consider h be Function of FGj, Bj such that
A9:  for x be Element of FGj holds h.x = G(x) from LambdaD;
    deffunc F(set) = IFEQ($1, j, g, r.$1);
    consider G be ManySortedSet of I such that
A10:  for i be set st i in I holds G.i = F(i) from MSSLambda;
    deffunc F(set) = IFEQ($1, j, h, r.$1);
    consider H be ManySortedSet of I such that
A11:  for i be set st i in I holds H.i = F(i) from MSSLambda;
      now
     let G be ManySortedSet of I;
     let g, h be Function of FGj, Bj such that
A12:   for i be set st i in I holds G.i = IFEQ(i, j, g, r.i);
     thus G is Function-yielding
     proof
      let i be set;
      assume i in dom G;
then A13:   i in I by PBOOLE:def 3;
        now per cases;
       case i = j;
       then IFEQ(i, j, g, r.i) = g by CQC_LANG:def 1;
       hence G.i is Function by A12,A13;
       case i <> j;
       then IFEQ(i, j, g, r.i) = r.i by CQC_LANG:def 1;
       hence G.i is Function by A12,A13;
      end;
      hence G.i is Function;
     end;
    end;
    then reconsider G, H as ManySortedFunction of I by A10,A11;
      now
     let G be ManySortedFunction of I;
     let g, h be Function of FGj, Bj such that
A14:   for i be set st i in I holds G.i = IFEQ(i, j, g, r.i);
     thus G is ManySortedFunction of FG, B
     proof
      let i be set such that
A15:    i in I;
        now per cases;
       case
A16:     i = j;
       then IFEQ(i, j, g, r.i) = g by CQC_LANG:def 1;
       hence G.i is Function of FG.i, B.i by A14,A15,A16;
       case i <> j;
       then IFEQ(i, j, g, r.i) = r.i by CQC_LANG:def 1;
       then G.i = r.i by A14,A15;
       hence G.i is Function of FG.i, B.i by A15,MSUALG_1:def 2;
      end;
      hence G.i is Function of FG.i, B.i;
     end;
    end;
    then reconsider G, H as ManySortedFunction of FG, B by A10,A11;
    consider h1 be ManySortedFunction of U1, U2 such that
A17:  h1 is_homomorphism U1, U2 & h1 || FG = G by A7,MSAFREE:def 5;
    consider h2 be ManySortedFunction of U1, U2 such that
A18:  h2 is_homomorphism U1, U2 & h2 || FG = H by A7,MSAFREE:def 5;
    take h1, h2;
    thus h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 by A17,A18;
      now
     let i be set; assume
A19:   i in I;
       now per cases;
      case
A20:    i = j;
then A21:      IFEQ(i, j, g, r.i) = g by CQC_LANG:def 1;
A22:      IFEQ(i, j, h, r.i) = h by A20,CQC_LANG:def 1;
A23:   f is Function of B.i, C.i by A4,A20,MSUALG_1:def 2;
      then reconsider fg = f*g as Function of FGj, C.i by A20,FUNCT_2:19;
      reconsider fh = f*h as Function of FGj, C.i by A20,A23,FUNCT_2:19;
        now
       let x be set; assume
A24:     x in FGj;
       hence fg.x = f.(g.x) by FUNCT_2:21
                .= f.x2' by A6,A8,A24
                .= f.(h.x) by A9,A24
                .= fh.x by A24,FUNCT_2:21;
      end;
then A25:   f*g = f*h by FUNCT_2:18;
A26:   h = (h2 || FG).i by A11,A18,A19,A22;
        g = (h1 || FG).i by A10,A17,A19,A21;
      then (F**(h1 || FG)).i = f*g by A4,A20,MSUALG_3:2;
      hence (F**(h1 || FG)).i = (F**(h2 || FG)).i
       by A4,A20,A25,A26,MSUALG_3:2;
      case
A27:    i <> j;
then A28:   IFEQ(i, j, g, r.i) = r.i by CQC_LANG:def 1;
A29:   IFEQ(i, j, h, r.i) = r.i by A27,CQC_LANG:def 1;
A30:   (h1 || FG).i = r.i by A10,A17,A19,A28
               .= (h2 || FG).i by A11,A18,A19,A29;
      reconsider h2' = (h2 || FG).i
       as Function of FG.i, B.i by A19,MSUALG_1:def 2;
      reconsider f' = F.i as Function of B.i, C.i by A19,MSUALG_1:def 2;
      thus (F**(h1 || FG)).i = f'*h2' by A19,A30,MSUALG_3:2
                            .= (F**(h2 || FG)).i by A19,MSUALG_3:2;
     end;
     hence (F**(h1 || FG)).i = (F**(h2 || FG)).i;
    end;
then A31: F**(h1 || FG) = F**(h2 || FG) by PBOOLE:3;
A32: (F**h1) || FG = F**(h1 || FG) by Th8
                 .= (F**h2) || FG by A31,Th8;
    reconsider Fh1 = F**h1, Fh2 = F**h2 as ManySortedFunction of U1, U3;
      Fh1 is_homomorphism U1, U3 & Fh2 is_homomorphism U1, U3
     by A1,A17,A18,MSUALG_3:10;
    hence F**h1 = F**h2 by A32,Th18;
      now
     take i = j;
     thus i in I by A4;
A33:  g = IFEQ(i, j, g, r.i) by CQC_LANG:def 1
      .= G.i by A4,A10;
A34:  h = IFEQ(i, j, h, r.i) by CQC_LANG:def 1
      .= H.i by A4,A11;
       now
      let x be Element of FGj;
      assume g = h;
      then g.x = x2' by A9;
      hence contradiction by A6,A8;
     end;
     hence G <> H by A33,A34;
    end;
    hence h1 <> h2 by A17,A18;
   end;
   hence contradiction by A2;
  end;

definition let S, U1;
 cluster non-empty GeneratorSet of U1;
existence
 proof
    the Sorts of U1 is GeneratorSet of U1 by MSAFREE2:9;
  then consider G be GeneratorSet of U1 such that
A1: G = the Sorts of U1;
  take G;
  thus thesis by A1;
 end;
end;

theorem
  for U1 being MSAlgebra over S
 for A, B being MSSubset of U1 st A is ManySortedSubset of B
 holds GenMSAlg A is MSSubAlgebra of GenMSAlg B
  proof
   let U1 be MSAlgebra over S,
       A, B be MSSubset of U1;
   assume A is ManySortedSubset of B;
then A1:A c= B by MSUALG_2:def 1;
     B is MSSubset of GenMSAlg B by MSUALG_2:def 18;
   then B c= the Sorts of GenMSAlg B by MSUALG_2:def 1;
   then A c= the Sorts of GenMSAlg B by A1,PBOOLE:15;
   then A is MSSubset of GenMSAlg B by MSUALG_2:def 1;
   hence thesis by MSUALG_2:def 18;
  end;

theorem
  for U1 being MSAlgebra over S, U2 being MSSubAlgebra of U1
  for B1 being MSSubset of U1, B2 being MSSubset of U2 st B1 = B2
 holds GenMSAlg B1 = GenMSAlg B2
  proof
   let U1 be MSAlgebra over S,
       U2 be MSSubAlgebra of U1,
       B1 be MSSubset of U1,
       B2 be MSSubset of U2 such that
A1:      B1 = B2;
   reconsider G = GenMSAlg B2 as MSSubAlgebra of U1 by MSUALG_2:7;
   reconsider H = GenMSAlg B1 as MSSubAlgebra of U2 by A1,MSUALG_2:def 18;
     B1 is MSSubset of H by MSUALG_2:def 18;
then A2:GenMSAlg B2 is MSSubAlgebra of GenMSAlg B1 by A1,MSUALG_2:def 18;
     B1 is MSSubset of G by A1,MSUALG_2:def 18;
   then GenMSAlg B1 is MSSubAlgebra of G by MSUALG_2:def 18;
   hence GenMSAlg B1 = GenMSAlg B2 by A2,MSUALG_2:8;
  end;

theorem
  for U1 being strict non-empty MSAlgebra over S
 for U2 being non-empty MSAlgebra over S
  for Gen being GeneratorSet of U1
   for h1, h2 being ManySortedFunction of U1, U2 st
    h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 &
     h1 || Gen = h2 || Gen
 holds h1 = h2
  proof
    let U1 be strict non-empty MSAlgebra over S,
        U2 be non-empty MSAlgebra over S,
        Gen be GeneratorSet of U1,
        h1, h2 be ManySortedFunction of U1, U2 such that
A1:  h1 is_homomorphism U1, U2 and
A2:  h2 is_homomorphism U1, U2 and
A3:  h1 || Gen = h2 || Gen;
set I = the carrier of S;

defpred P[set,set] means
 ex s being SortSymbol of S st $1 = s & h1.s.$2 = h2.s.$2;

    consider A being ManySortedSet of I such that
A4:   for i being set st i in I
       for e being set holds e in A.i iff e in (the Sorts of U1).i & P[i,e]
        from PSeparation;
      A is ManySortedSubset of the Sorts of U1
    proof
      let i be set such that
A5:     i in I;
      let e be set;
      assume e in A.i;
      hence thesis by A4,A5;
    end;
    then reconsider A as MSSubset of U1;
      A is opers_closed
    proof
      let o be OperSymbol of S;
      let y be set;
set r = the_result_sort_of o;
set ar = the_arity_of o;
      assume y in rng ((Den(o,U1))|((A# * the Arity of S).o));
      then consider x being set such that
A6:     x in dom ((Den(o,U1))|((A# * the Arity of S).o)) and
A7:     ((Den(o,U1))|((A# * the Arity of S).o)).x = y by FUNCT_1:def 5;
A8:   x in (A# * the Arity of S).o by A6,RELAT_1:86;
      then x in A#.((the Arity of S).o) by FUNCT_2:21;
      then x in A#.ar by MSUALG_1:def 6;
then A9:   x in product(A*ar) by MSUALG_1:def 3;
      reconsider x as Element of Args(o,U1) by A6;
A10:   y = Den(o,U1).x by A7,A8,FUNCT_1:72;
        Den(o,U1).x is Element of ((the Sorts of U1)*the ResultSort of S).o
        by MSUALG_1:def 10;
      then Den(o,U1).x is Element of (the Sorts of U1).((the ResultSort of S).
o)
        by FUNCT_2:21;
      then A11: Den(o,U1).x is Element of (the Sorts of U1).r by MSUALG_1:def 7
;
A12:   dom (h1#x) = dom ar by MSUALG_3:6;
A13:   dom (h2#x) = dom ar by MSUALG_3:6;
A14:   for n being set st n in dom (h1#x) holds (h1#x).n = (h2#x).n
      proof
        let n be set such that
A15:       n in dom (h1#x);
A16:     dom x = dom ar by MSUALG_3:6;
          dom x = dom (A*ar) by A9,CARD_3:18;
        then x.n in (A*ar).n by A9,A12,A15,A16,CARD_3:18;
        then x.n in A.(ar.n) by A12,A15,FUNCT_1:23;
        then x.n in A.(ar/.n) by A12,A15,FINSEQ_4:def 4;
then ex s being SortSymbol of S st s = ar/.n & h1.s.(x.n) = h2.s.(x.n)
         by A4;
        hence (h1#x).n = h2.(ar/.n).(x.n) by A12,A15,A16,MSUALG_3:def 8
                     .= (h2#x).n by A12,A15,A16,MSUALG_3:def 8;
      end;
        h1.r.y = h1.r.(Den(o,U1).x) by A7,A8,FUNCT_1:72
            .= Den(o,U2).(h1#x) by A1,MSUALG_3:def 9
            .= Den(o,U2).(h2#x) by A12,A13,A14,FUNCT_1:9
            .= h2.r.(Den(o,U1).x) by A2,MSUALG_3:def 9
            .= h2.r.y by A7,A8,FUNCT_1:72;
      then y in A.r by A4,A10,A11;
      then y in A.((the ResultSort of S).o) by MSUALG_1:def 7;
      hence y in (A * the ResultSort of S).o by FUNCT_2:21;
    end;
then A17: U1|A = MSAlgebra (#A , Opers(U1,A)#) by MSUALG_2:def 16;
      Gen is ManySortedSubset of the Sorts of U1|A
    proof
      let i be set such that
A18:     i in I;
      let x be set such that
A19:     x in Gen.i;
        Gen c= the Sorts of U1 by MSUALG_2:def 1;
then A20:   Gen.i c= (the Sorts of U1).i by A18,PBOOLE:def 5;
      reconsider s = i as SortSymbol of S by A18;
        h1.s.x = ((h1.s) | (Gen.s)).x by A19,FUNCT_1:72
            .= (h1 || Gen).s.x by MSAFREE:def 1
            .= ((h2.s) | (Gen.s)).x by A3,MSAFREE:def 1
            .= h2.s.x by A19,FUNCT_1:72;
      hence x in (the Sorts of U1|A).i by A4,A17,A19,A20;
    end;
then A21: GenMSAlg Gen is MSSubAlgebra of U1|A by MSUALG_2:def 18;
      the Sorts of GenMSAlg Gen = the Sorts of U1 by MSAFREE:def 4;
    then the Sorts of U1 is ManySortedSubset of A by A17,A21,MSUALG_2:def 10;
      then A22: the Sorts of U1 c= A by MSUALG_2:def 1;
      now
      let i be set; assume
A23:     i in I;
      then reconsider s = i as SortSymbol of S;
A24:   dom (h1.s) = (the Sorts of U1).i by FUNCT_2:def 1;
A25:   dom (h2.s) = (the Sorts of U1).i by FUNCT_2:def 1;
        now
        let x be set such that
A26:       x in dom (h1.s);
          (the Sorts of U1).i c= A.i by A22,A23,PBOOLE:def 5;
        then ex t being SortSymbol of S st t = s & h1.t.x = h2.t.x by A4,A24,
A26;
        hence h1.s.x = h2.s.x;
      end;
      hence h1.i = h2.i by A24,A25,FUNCT_1:9;
    end;
    hence h1 = h2 by PBOOLE:3;
  end;

Back to top