extens_1.miz



    begin

    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 holds for A,B,C be ManySortedSet of I holds for F be ManySortedFunction of A, B holds 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 PBOOLE:def 19

      .= (I /\ ( dom G)) by PARTFUN1:def 2

      .= (I /\ I) by PARTFUN1:def 2

      .= I;

      hence thesis by PARTFUN1:def 2, RELAT_1:def 18;

    end;

    begin

    theorem :: EXTENS_1:1

    for F be ManySortedFunction of A, B holds 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 object;

        assume

         A2: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        

         A3: (A . i) c= (X . i) by A1, A2;

        

        thus ((F || X) . i) = (f | (X . i)) by A2, MSAFREE:def 1

        .= (F . i) by A3, RELSET_1: 19;

      end;

      hence thesis;

    end;

    theorem :: EXTENS_1:2

    for A,B be ManySortedSet of I holds for M be ManySortedSubset of A holds 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 object such that

       A1: i in I;

      reconsider f = (F . i) as Function of (A . i), (B . i) by A1, PBOOLE:def 15;

      

       A2: ((F .:.: M) . i) = (f .: (M . i)) by A1, PBOOLE:def 20;

      M c= A by PBOOLE:def 18;

      then (M . i) c= (A . i) by A1;

      then

       A3: (f .: (M . i)) c= (f .: (A . i)) by RELAT_1: 123;

      let x be object;

      assume x in ((F .:.: M) . i);

      then x in (f .: (A . i)) by A2, A3;

      hence thesis by A1, PBOOLE:def 20;

    end;

    theorem :: EXTENS_1:3

    for F be ManySortedFunction of A, B holds 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 object;

        assume

         A2: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider fm = ((F || M2) . i) as Function of (M2 . i), (B . i) by A2, PBOOLE:def 15;

        

         A3: (M1 . i) c= (M2 . i) by A1, A2;

        fm = (f | (M2 . i)) by A2, MSAFREE:def 1;

        

        hence (((F || M2) .:.: M1) . i) = ((f | (M2 . i)) .: (M1 . i)) by A2, PBOOLE:def 20

        .= (f .: (M1 . i)) by A3, RELAT_1: 129

        .= ((F .:.: M1) . i) by A2, PBOOLE:def 20;

      end;

      hence thesis;

    end;

    theorem :: EXTENS_1:4

    

     Th4: for F be ManySortedFunction of A, B holds for G be ManySortedFunction of B, C holds 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 object;

        assume

         A1: i in I;

        then

        reconsider gf = ((G ** F) . i) as Function of (A . i), (C . i) by PBOOLE:def 15;

        reconsider fx = ((F || X) . i) as Function of (X . i), (B . i) by A1, PBOOLE:def 15;

        reconsider g = (G . i) as Function of (B . i), (C . i) by A1, PBOOLE:def 15;

        reconsider f = (F . i) as Function of (A . i), (B . i) by A1, PBOOLE:def 15;

        

        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: 83

        .= (g * fx) by A1, MSAFREE:def 1

        .= ((G ** (F || X)) . i) by A1, MSUALG_3: 2;

      end;

      hence thesis;

    end;

    theorem :: EXTENS_1:5

    for A,B be ManySortedSet of I st A is_transformable_to B holds for F be ManySortedFunction of A, B holds 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;

      assume B is ManySortedSubset of C;

      then

       A2: B c= C by PBOOLE:def 18;

      let i be object such that

       A3: i in I;

      

       A4: (B . i) = {} implies (A . i) = {} by A1, A3, PZFMISC1:def 3;

      

       A5: (F . i) is Function of (A . i), (B . i) by A3, PBOOLE:def 15;

      (B . i) c= (C . i) by A3, A2;

      hence thesis by A4, A5, FUNCT_2: 7;

    end;

    theorem :: EXTENS_1:6

    for F be ManySortedFunction of A, B holds 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 PBOOLE:def 15;

        f is one-to-one by A1, A2, MSUALG_3: 1;

        then (f | (X . i)) is one-to-one by FUNCT_1: 52;

        hence ((F || X) . i) is one-to-one by A2, MSAFREE:def 1;

      end;

      hence thesis by MSUALG_3: 1;

    end;

    begin

    theorem :: EXTENS_1:7

    for F be ManySortedFunction of A, B holds 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 object;

      

       A1: ( dom (F || X)) = I by PARTFUN1:def 2;

      assume

       A2: i in I;

      then

      reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

      ( dom F) = I by PARTFUN1:def 2;

      then

       A3: (( doms F) . i) = ( dom f) by A2, FUNCT_6: 22;

      ((F || X) . i) = (f | (X . i)) by A2, MSAFREE:def 1;

      then (( doms (F || X)) . i) = ( dom (f | (X . i))) by A2, A1, FUNCT_6: 22;

      hence thesis by A3, RELAT_1: 60;

    end;

    theorem :: EXTENS_1:8

    for F be ManySortedFunction of A, B holds 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 object;

      

       A1: ( dom (F || X)) = I by PARTFUN1:def 2;

      assume

       A2: i in I;

      then

      reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

      ( dom F) = I by PARTFUN1:def 2;

      then

       A3: (( rngs F) . i) = ( rng f) by A2, FUNCT_6: 22;

      ((F || X) . i) = (f | (X . i)) by A2, MSAFREE:def 1;

      then (( rngs (F || X)) . i) = ( rng (f | (X . i))) by A2, A1, FUNCT_6: 22;

      hence thesis by A3, RELAT_1: 70;

    end;

    theorem :: EXTENS_1:9

    for A,B be ManySortedSet of I holds 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 PARTFUN1:def 2;

      thus F is "onto" implies ( rngs F) = B

      proof

        assume

         A2: F is "onto";

        now

          let i be object;

          assume

           A3: i in I;

          then

          reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

          ( rng f) = (B . i) by A2, A3;

          hence (( rngs F) . i) = (B . i) by A1, A3, FUNCT_6: 22;

        end;

        hence thesis;

      end;

      assume

       A4: ( rngs F) = B;

      let i be set;

      assume i in I;

      hence thesis by A1, A4, FUNCT_6: 22;

    end;

    theorem :: EXTENS_1:10

    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 object such that

         A1: i in I;

        reconsider r = (R . i) as Function of (( FreeGen X) . i), (X . i) by A1, PBOOLE:def 15;

        

         A2: ( dom R) = I by PARTFUN1:def 2;

        thus (( rngs R) . i) = (X . i)

        proof

          reconsider s0 = i as SortSymbol of S by A1;

          set D = ( DTConMSA X);

          thus (( rngs R) . i) c= (X . i)

          proof

            let x be object;

            assume x in (( rngs R) . i);

            then

             A3: x in ( rng r) by A1, A2, FUNCT_6: 22;

            ( rng r) c= (X . i) by RELAT_1:def 19;

            hence thesis by A3;

          end;

          let x be object;

          assume x in (X . i);

          then

           A4: [x, s0] in ( Terminals D) by MSAFREE: 7;

          then

          reconsider t = [x, s0] as Symbol of D;

          (t `2 ) = s0;

          then ( root-tree t) in { ( root-tree tt) where tt be Symbol of D : tt in ( Terminals D) & (tt `2 ) = s0 } by A4;

          then

           A5: ( root-tree t) in ( FreeGen (s0,X)) by MSAFREE: 13;

          

           A6: (R . s0) = ( Reverse (s0,X)) by MSAFREE:def 18;

          

          then

           A7: ((R . s0) . ( root-tree t)) = (t `1 ) by A5, MSAFREE:def 17

          .= x;

          ( dom (R . s0)) = ( FreeGen (s0,X)) by A6, FUNCT_2:def 1;

          then ((R . s0) . ( root-tree t)) in ( rng (R . s0)) by A5, FUNCT_1:def 3;

          hence thesis by A2, A7, FUNCT_6: 22;

        end;

      end;

      hence thesis;

    end;

    theorem :: EXTENS_1:11

    for F be ManySortedFunction of A, B holds for G be ManySortedFunction of B, C holds 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 PARTFUN1:def 2;

      

       A3: F is ManySortedFunction of A, X

      proof

        let i be object;

        assume

         A4: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        

         A5: (( rngs F) . i) c= (X . i) by A1, A4;

        ( dom f) = (A . i) & (( rngs F) . i) = ( rng f) by A2, A4, FUNCT_2:def 1, FUNCT_6: 22;

        hence thesis by A4, A5, FUNCT_2:def 1, RELSET_1: 4;

      end;

       A6:

      now

        let i be object;

        assume

         A7: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        (( rngs F) . i) = ( rng f) by A2, A7, FUNCT_6: 22;

        then

         A8: ( rng f) c= (X . i) by A1, A7;

        ( dom f) = (A . i) by A7, FUNCT_2:def 1;

        then

        reconsider f9 = f as Function of (A . i), (X . i) by A7, A8, FUNCT_2:def 1, RELSET_1: 4;

        reconsider g = (G . i) as Function of (B . i), (C . i) by A7, PBOOLE:def 15;

        

         A9: ( rng f9) c= (X . i) by RELAT_1:def 19;

        reconsider gx = ((G || X) . i) as Function of (X . i), (C . i) by A7, PBOOLE:def 15;

        

        thus (((G || X) ** F) . i) = (gx * f9) by A3, A7, MSUALG_3: 2

        .= ((g | (X . i)) * f) by A7, MSAFREE:def 1

        .= (g * f9) by A9, MSUHOM_1: 1

        .= ((G ** F) . i) by A7, MSUALG_3: 2;

      end;

      ((G || X) ** F) is ManySortedSet of I by A3, Lm1;

      hence thesis by A6, PBOOLE: 3;

    end;

    begin

    theorem :: EXTENS_1:12

    

     Th12: for F be ManySortedFunction of A, B holds F is "onto" iff for C holds 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 holds 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 object;

          assume

           A3: i in I;

          then

          reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

          reconsider h = (H . i) as Function of (B . i), (C . i) by A3, PBOOLE:def 15;

          reconsider g = (G . i) as Function of (B . i), (C . i) by A3, PBOOLE:def 15;

          

           A4: ( rng f) = (B . i) by A1, A3;

          (g * f) = ((H ** F) . i) by A2, A3, MSUALG_3: 2

          .= (h * f) by A3, MSUALG_3: 2;

          hence (G . i) = (H . i) by A3, A4, FUNCT_2: 16;

        end;

        hence thesis;

      end;

      assume that

       A5: for C holds for G,H be ManySortedFunction of B, C st (G ** F) = (H ** F) holds G = H and

       A6: not F is "onto";

      consider j be set such that

       A7: j in I and

       A8: ( rng (F . j)) <> (B . j) by A6;

      reconsider I as non empty set by A7;

      reconsider j as Element of I by A7;

      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);

      consider Z be set such that

       A9: Z <> {} and

       A10: ex g,h be Function of (B . j), Z st (g * f) = (h * f) & g <> h by A8, FUNCT_2: 16;

      consider g,h be Function of (B . j), Z such that

       A11: (g * (F . j)) = (h * (F . j)) and

       A12: g <> h by A10;

      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( object) = ( IFEQ ($1,j,Z,(B . $1)));

        consider C be ManySortedSet of I such that

         A13: for i be object st i in I holds (C . i) = F(i) from PBOOLE:sch 4;

        take C;

        thus C is non-empty

        proof

          let i be object such that

           A14: i in I;

          now

            per cases ;

              case i = j;

              then ( IFEQ (i,j,Z,(B . i))) = Z by FUNCOP_1:def 8;

              hence thesis by A9, A13, A14;

            end;

              case i <> j;

              then ( IFEQ (i,j,Z,(B . i))) = (B . i) by FUNCOP_1:def 8;

              hence thesis by A13, A14;

            end;

          end;

          hence thesis;

        end;

        deffunc F( object) = ( IFEQ ($1,j,g,(( id B) . $1)));

        consider G be ManySortedSet of I such that

         A15: for i be object st i in I holds (G . i) = F(i) from PBOOLE:sch 4;

        deffunc F( object) = ( IFEQ ($1,j,h,(( id B) . $1)));

        consider H be ManySortedSet of I such that

         A16: for i be object st i in I holds (H . i) = F(i) from PBOOLE:sch 4;

        now

          let G be ManySortedSet of I;

          let g,h be Function of (B . j), Z such that (g * (F . j)) = (h * (F . j)) and g <> h and

           A17: for i be object st i in I holds (G . i) = ( IFEQ (i,j,g,(( id B) . i)));

          thus G is Function-yielding

          proof

            let i be object;

            assume i in ( dom G);

            then

             A18: i in I;

            now

              per cases ;

                case i = j;

                then ( IFEQ (i,j,g,(( id B) . i))) = g by FUNCOP_1:def 8;

                hence thesis by A17, A18;

              end;

                case i <> j;

                then ( IFEQ (i,j,g,(( id B) . i))) = (( id B) . i) by FUNCOP_1:def 8;

                hence thesis by A17, A18;

              end;

            end;

            hence thesis;

          end;

        end;

        then

        reconsider G, H as ManySortedFunction of I by A11, A12, A15, A16;

        now

          let G be ManySortedFunction of I;

          let g,h be Function of (B . j), Z such that (g * (F . j)) = (h * (F . j)) and g <> h and

           A19: for i be object 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 object such that

             A20: i in I;

            now

              per cases ;

                case

                 A21: i = j;

                then

                 A22: ( IFEQ (i,j,Z,(B . i))) = Z by FUNCOP_1:def 8;

                ( IFEQ (i,j,g,(( id B) . i))) = g & (C . i) = ( IFEQ (i,j,Z,(B . i))) by A13, A21, FUNCOP_1:def 8;

                hence thesis by A19, A21, A22;

              end;

                case

                 A23: i <> j;

                then ( IFEQ (i,j,Z,(B . i))) = (B . i) by FUNCOP_1:def 8;

                then

                 A24: (B . i) = (C . i) by A13, A20;

                ( IFEQ (i,j,g,(( id B) . i))) = (( id B) . i) by A23, FUNCOP_1:def 8;

                then (G . i) = (( id B) . i) by A19, A20;

                hence thesis by A20, A24, PBOOLE:def 15;

              end;

            end;

            hence thesis;

          end;

        end;

        then

        reconsider G, H as ManySortedFunction of B, C by A11, A12, A15, A16;

         A25:

        now

          let i be object such that

           A26: i in I;

          now

            per cases ;

              case

               A27: i = j;

              then ( IFEQ (i,j,h,(( id B) . i))) = h by FUNCOP_1:def 8;

              then

               A28: h = (H . i) by A16, A26;

              ( IFEQ (i,j,g,(( id B) . i))) = g by A27, FUNCOP_1:def 8;

              then g = (G . i) by A15, A26;

              

              hence ((G ** F) . i) = (h * (F . j)) by A11, A27, MSUALG_3: 2

              .= ((H ** F) . i) by A27, A28, MSUALG_3: 2;

            end;

              case

               A29: i <> j;

              reconsider g9 = (G . i) as Function of (B . i), (C . i) by A26, PBOOLE:def 15;

              reconsider f9 = (F . i) as Function of (A . i), (B . i) by A26, PBOOLE:def 15;

              reconsider h9 = (H . i) as Function of (B . i), (C . i) by A26, PBOOLE:def 15;

              

               A30: ( IFEQ (i,j,h,(( id B) . i))) = (( id B) . i) by A29, FUNCOP_1:def 8;

              ( IFEQ (i,j,g,(( id B) . i))) = (( id B) . i) by A29, FUNCOP_1:def 8;

              

              then g9 = (( id B) . i) by A15, A26

              .= h9 by A16, A26, A30;

              

              hence ((G ** F) . i) = (h9 * f9) by A26, MSUALG_3: 2

              .= ((H ** F) . i) by A26, MSUALG_3: 2;

            end;

          end;

          hence ((G ** F) . i) = ((H ** F) . i);

        end;

        take G, H;

        (G ** F) is ManySortedSet of I & (H ** F) is ManySortedSet of I by Lm1;

        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;

          

           A31: h = ( IFEQ (i,j,h,(( id B) . i))) by FUNCOP_1:def 8

          .= (H . i) by A16;

          g = ( IFEQ (i,j,g,(( id B) . i))) by FUNCOP_1:def 8

          .= (G . i) by A15;

          hence thesis by A12, A31;

        end;

        hence thesis;

      end;

      hence contradiction by A5;

    end;

    theorem :: EXTENS_1:13

    

     Th13: for F be ManySortedFunction of A, B st A is non-empty holds F is "1-1" iff for C be ManySortedSet of I holds 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;

      thus F is "1-1" implies for C be ManySortedSet of I holds 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 object;

          assume

           A4: i in I;

          then

          reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

          reconsider h = (H . i) as Function of (C . i), (A . i) by A4, PBOOLE:def 15;

          reconsider g = (G . i) as Function of (C . i), (A . i) by A4, PBOOLE:def 15;

          

           A5: 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 A1, A4, A5, FUNCT_2: 21;

        end;

        hence thesis;

      end;

      assume that

       A6: for C be ManySortedSet of I holds for G,H be ManySortedFunction of C, A st (F ** G) = (F ** H) holds G = H and

       A7: not F is "1-1";

      consider j be set such that

       A8: j in I and

       A9: not (F . j) is one-to-one by A7, MSUALG_3: 1;

      (F . j) is Function of (A . j), (B . j) by A8, PBOOLE:def 15;

      then

      consider Z be set such that

       A10: ex g,h be Function of Z, (A . j) st ((F . j) * g) = ((F . j) * h) & g <> h by A1, A8, A9, FUNCT_2: 21;

      consider g,h be Function of Z, (A . j) such that

       A11: ((F . j) * g) = ((F . j) * h) and

       A12: g <> h by A10;

      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( object) = ( IFEQ ($1,j,Z,(A . $1)));

        consider C be ManySortedSet of I such that

         A13: for i be object st i in I holds (C . i) = F(i) from PBOOLE:sch 4;

        take C;

        deffunc F( object) = ( IFEQ ($1,j,g,(( id C) . $1)));

        consider G be ManySortedSet of I such that

         A14: for i be object st i in I holds (G . i) = F(i) from PBOOLE:sch 4;

        deffunc F( object) = ( IFEQ ($1,j,h,(( id C) . $1)));

        consider H be ManySortedSet of I such that

         A15: for i be object st i in I holds (H . i) = F(i) from PBOOLE:sch 4;

        now

          let G be ManySortedSet of I;

          let g,h be Function of Z, (A . j) such that ((F . j) * g) = ((F . j) * h) and g <> h and

           A16: for i be object st i in I holds (G . i) = ( IFEQ (i,j,g,(( id C) . i)));

          thus G is Function-yielding

          proof

            let i be object;

            assume i in ( dom G);

            then

             A17: i in I;

            now

              per cases ;

                case i = j;

                then ( IFEQ (i,j,g,(( id C) . i))) = g by FUNCOP_1:def 8;

                hence thesis by A16, A17;

              end;

                case i <> j;

                then ( IFEQ (i,j,g,(( id C) . i))) = (( id C) . i) by FUNCOP_1:def 8;

                hence thesis by A16, A17;

              end;

            end;

            hence thesis;

          end;

        end;

        then

        reconsider G, H as ManySortedFunction of I by A11, 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) and g <> h and

           A18: for i be object 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 object such that

             A19: i in I;

            now

              per cases ;

                case

                 A20: i = j;

                then

                 A21: ( IFEQ (i,j,g,(( id C) . i))) = g & ( IFEQ (i,j,Z,(A . i))) = Z by FUNCOP_1:def 8;

                (C . i) = ( IFEQ (i,j,Z,(A . i))) by A13, A19;

                hence thesis by A18, A19, A20, A21;

              end;

                case

                 A22: i <> j;

                then ( IFEQ (i,j,Z,(A . i))) = (A . i) by FUNCOP_1:def 8;

                then

                 A23: (C . i) = (A . i) by A13, A19;

                ( IFEQ (i,j,g,(( id C) . i))) = (( id C) . i) by A22, FUNCOP_1:def 8;

                then (G . i) = (( id C) . i) by A18, A19;

                hence thesis by A19, A23, PBOOLE:def 15;

              end;

            end;

            hence thesis;

          end;

        end;

        then

        reconsider G, H as ManySortedFunction of C, A by A11, A12, A14, A15;

         A24:

        now

          let i be object such that

           A25: i in I;

          now

            per cases ;

              case

               A26: i = j;

              then ( IFEQ (i,j,h,(( id C) . i))) = h by FUNCOP_1:def 8;

              then

               A27: h = (H . i) by A15, A25;

              ( IFEQ (i,j,g,(( id C) . i))) = g by A26, FUNCOP_1:def 8;

              then g = (G . i) by A14, A25;

              

              hence ((F ** G) . i) = ((F . j) * h) by A8, A11, A26, MSUALG_3: 2

              .= ((F ** H) . i) by A8, A26, A27, MSUALG_3: 2;

            end;

              case

               A28: i <> j;

              reconsider g9 = (G . i) as Function of (C . i), (A . i) by A25, PBOOLE:def 15;

              reconsider f9 = (F . i) as Function of (A . i), (B . i) by A25, PBOOLE:def 15;

              reconsider h9 = (H . i) as Function of (C . i), (A . i) by A25, PBOOLE:def 15;

              

               A29: ( IFEQ (i,j,h,(( id C) . i))) = (( id C) . i) by A28, FUNCOP_1:def 8;

              ( IFEQ (i,j,g,(( id C) . i))) = (( id C) . i) by A28, FUNCOP_1:def 8;

              

              then g9 = (( id C) . i) by A14, A25

              .= h9 by A15, A25, A29;

              

              hence ((F ** G) . i) = (f9 * h9) by A25, MSUALG_3: 2

              .= ((F ** H) . i) by A25, MSUALG_3: 2;

            end;

          end;

          hence ((F ** G) . i) = ((F ** H) . i);

        end;

        take G, H;

        (F ** G) is ManySortedSet of I & (F ** H) is ManySortedSet of I by Lm1;

        hence (F ** G) = (F ** H) by A24, PBOOLE: 3;

        ex i be set st i in I & (G . i) <> (H . i)

        proof

          take i = j;

          thus i in I by A8;

          

           A30: h = ( IFEQ (i,j,h,(( id C) . i))) by FUNCOP_1:def 8

          .= (H . i) by A8, A15;

          g = ( IFEQ (i,j,g,(( id C) . i))) by FUNCOP_1:def 8

          .= (G . i) by A8, A14;

          hence thesis by A12, A30;

        end;

        hence thesis;

      end;

      hence contradiction by A6;

    end;

    begin

    theorem :: EXTENS_1:14

    

     Th14: for X be non-empty ManySortedSet of the carrier of S holds 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: h2 is_homomorphism (( FreeMSA X),U1) by A2;

      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 ((h2 . s) . y) = x iff P[s, x, y]

      proof

        set FG = ( FreeGen X);

        let s be SortSymbol of S, x,y be set;

        assume y in ( FreeGen (s,X));

        then

         A6: y in (FG . s) by MSAFREE:def 16;

        

         A7: ((h1 || FG) . s) = ((h1 . s) | (FG . s)) & ((h2 || FG) . s) = ((h2 . s) | (FG . s)) by MSAFREE:def 1;

        (((h1 . s) | (FG . s)) . y) = ((h1 . s) . y) by A6, FUNCT_1: 49;

        hence thesis by A3, A7, A6, FUNCT_1: 49;

      end;

      

       A8: 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];

      

       A9: h1 is_homomorphism (( FreeMSA X),U1) by A1;

      thus h1 = h2 from MSAFREE1:sch 3( A9, A8, A4, A5);

    end;

    theorem :: EXTENS_1:15

    for F be ManySortedFunction of U1, U2 st F is_epimorphism (U1,U2) holds for U3 be non-empty MSAlgebra over S holds for h1,h2 be ManySortedFunction of U2, U3 st (h1 ** F) = (h2 ** F) holds h1 = h2 by Th12;

    theorem :: EXTENS_1:16

    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 holds 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);

      set C = the Sorts of U3;

      set B = the Sorts of U2;

      thus F is_monomorphism (U2,U3) implies for U1 be non-empty MSAlgebra over S holds 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) by Th13;

      set I = the carrier of S;

      assume that

       A2: for U1 be non-empty MSAlgebra over S holds 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);

       not F is "1-1" by A1, A3;

      then

      consider j be set such that

       A4: j in I and

       A5: not (F . j) is one-to-one by MSUALG_3: 1;

      set f = (F . j);

      (F . j) is Function of (B . j), (C . j) by A4, PBOOLE:def 15;

      then

      consider x1,x2 be object such that

       A6: x1 in (B . j) and

       A7: x2 in (B . j) and

       A8: (f . x1) = (f . x2) and

       A9: x1 <> x2 by A4, A5, FUNCT_2: 19;

      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;

        FG is non-empty by MSAFREE: 14;

        then

        reconsider FGj = (FG . j), Bj = (B . j) as non empty set by A4;

        reconsider h = (FGj --> x2) as Function of FGj, Bj by A7, FUNCOP_1: 45;

        reconsider g = (FGj --> x1) as Function of FGj, Bj by A6, FUNCOP_1: 45;

        set r = ( Reverse B);

        deffunc F( object) = ( IFEQ ($1,j,g,(r . $1)));

        consider G be ManySortedSet of I such that

         A10: for i be object st i in I holds (G . i) = F(i) from PBOOLE:sch 4;

        deffunc F( object) = ( IFEQ ($1,j,h,(r . $1)));

        consider H be ManySortedSet of I such that

         A11: for i be object st i in I holds (H . i) = F(i) from PBOOLE:sch 4;

        now

          let G be ManySortedSet of I;

          let g,h be Function of FGj, Bj such that

           A12: for i be object st i in I holds (G . i) = ( IFEQ (i,j,g,(r . i)));

          thus G is Function-yielding

          proof

            let i be object;

            assume i in ( dom G);

            then

             A13: i in I;

            now

              per cases ;

                case i = j;

                then ( IFEQ (i,j,g,(r . i))) = g by FUNCOP_1:def 8;

                hence thesis by A12, A13;

              end;

                case i <> j;

                then ( IFEQ (i,j,g,(r . i))) = (r . i) by FUNCOP_1:def 8;

                hence thesis by A12, A13;

              end;

            end;

            hence thesis;

          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 object st i in I holds (G . i) = ( IFEQ (i,j,g,(r . i)));

          thus G is ManySortedFunction of FG, B

          proof

            let i be object such that

             A15: i in I;

            now

              per cases ;

                case

                 A16: i = j;

                then ( IFEQ (i,j,g,(r . i))) = g by FUNCOP_1:def 8;

                hence thesis by A14, A15, A16;

              end;

                case i <> j;

                then ( IFEQ (i,j,g,(r . i))) = (r . i) by FUNCOP_1:def 8;

                then (G . i) = (r . i) by A14, A15;

                hence thesis by A15, PBOOLE:def 15;

              end;

            end;

            hence thesis;

          end;

        end;

        then

        reconsider G, H as ManySortedFunction of FG, B by A10, A11;

        

         A17: FG is free by MSAFREE: 16;

        then

        consider h1 be ManySortedFunction of U1, U2 such that

         A18: h1 is_homomorphism (U1,U2) and

         A19: (h1 || FG) = G by MSAFREE:def 5;

        consider h2 be ManySortedFunction of U1, U2 such that

         A20: h2 is_homomorphism (U1,U2) and

         A21: (h2 || FG) = H by A17, MSAFREE:def 5;

        take h1, h2;

        thus h1 is_homomorphism (U1,U2) & h2 is_homomorphism (U1,U2) by A18, A20;

        reconsider Fh1 = (F ** h1), Fh2 = (F ** h2) as ManySortedFunction of U1, U3;

        

         A22: Fh1 is_homomorphism (U1,U3) by A1, A18, MSUALG_3: 10;

        now

          let i be object;

          assume

           A23: i in I;

          now

            per cases ;

              case

               A24: i = j;

              then

               A25: f is Function of (B . i), (C . i) by A4, PBOOLE:def 15;

              then

              reconsider fg = (f * g) as Function of FGj, (C . i) by A24, FUNCT_2: 13;

              reconsider fh = (f * h) as Function of FGj, (C . i) by A24, A25, FUNCT_2: 13;

              now

                let x be object;

                assume

                 A26: x in FGj;

                

                hence (fg . x) = (f . (g . x)) by FUNCT_2: 15

                .= (f . x2) by A8, A26, FUNCOP_1: 7

                .= (f . (h . x)) by A26, FUNCOP_1: 7

                .= (fh . x) by A26, FUNCT_2: 15;

              end;

              then

               A27: (f * g) = (f * h) by FUNCT_2: 12;

              ( IFEQ (i,j,g,(r . i))) = g by A24, FUNCOP_1:def 8;

              then g = ((h1 || FG) . i) by A10, A19, A23;

              then

               A28: ((F ** (h1 || FG)) . i) = (f * g) by A4, A24, MSUALG_3: 2;

              ( IFEQ (i,j,h,(r . i))) = h by A24, FUNCOP_1:def 8;

              then h = ((h2 || FG) . i) by A11, A21, A23;

              hence ((F ** (h1 || FG)) . i) = ((F ** (h2 || FG)) . i) by A4, A24, A27, A28, MSUALG_3: 2;

            end;

              case

               A29: i <> j;

              reconsider f9 = (F . i) as Function of (B . i), (C . i) by A23, PBOOLE:def 15;

              reconsider h29 = ((h2 || FG) . i) as Function of (FG . i), (B . i) by A23, PBOOLE:def 15;

              

               A30: ( IFEQ (i,j,h,(r . i))) = (r . i) by A29, FUNCOP_1:def 8;

              ( IFEQ (i,j,g,(r . i))) = (r . i) by A29, FUNCOP_1:def 8;

              

              then ((h1 || FG) . i) = (r . i) by A10, A19, A23

              .= ((h2 || FG) . i) by A11, A21, A23, A30;

              

              hence ((F ** (h1 || FG)) . i) = (f9 * h29) by A23, MSUALG_3: 2

              .= ((F ** (h2 || FG)) . i) by A23, MSUALG_3: 2;

            end;

          end;

          hence ((F ** (h1 || FG)) . i) = ((F ** (h2 || FG)) . i);

        end;

        then

         A31: (F ** (h1 || FG)) = (F ** (h2 || FG));

        

         A32: Fh2 is_homomorphism (U1,U3) by A1, A20, MSUALG_3: 10;

        ((F ** h1) || FG) = (F ** (h1 || FG)) by Th4

        .= ((F ** h2) || FG) by A31, Th4;

        hence (F ** h1) = (F ** h2) by A22, A32, Th14;

        now

          take i = j;

          thus i in I by A4;

           A33:

          now

            let x be Element of FGj;

            assume g = h;

            then (g . x) = x2 by FUNCOP_1: 7;

            hence contradiction by A9;

          end;

          

           A34: h = ( IFEQ (i,j,h,(r . i))) by FUNCOP_1:def 8

          .= (H . i) by A4, A11;

          g = ( IFEQ (i,j,g,(r . i))) by FUNCOP_1:def 8

          .= (G . i) by A4, A10;

          hence G <> H by A34, A33;

        end;

        hence thesis by A19, A21;

      end;

      hence contradiction by A2;

    end;

    registration

      let S, U1;

      cluster non-empty for GeneratorSet of U1;

      existence

      proof

        the Sorts of U1 is GeneratorSet of U1 by MSAFREE2: 6;

        then

        consider G be GeneratorSet of U1 such that

         A1: G = the Sorts of U1;

        take G;

        thus thesis by A1;

      end;

    end

    theorem :: EXTENS_1:17

    for U1 be MSAlgebra over S holds for A,B be 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;

      B is MSSubset of ( GenMSAlg B) by MSUALG_2:def 17;

      then

       A1: B c= the Sorts of ( GenMSAlg B) by PBOOLE:def 18;

      assume A is ManySortedSubset of B;

      then A c= B by PBOOLE:def 18;

      then A c= the Sorts of ( GenMSAlg B) by A1, PBOOLE: 13;

      then A is MSSubset of ( GenMSAlg B) by PBOOLE:def 18;

      hence thesis by MSUALG_2:def 17;

    end;

    theorem :: EXTENS_1:18

    for U1 be MSAlgebra over S, U2 be MSSubAlgebra of U1 holds for B1 be MSSubset of U1, B2 be 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 H = ( GenMSAlg B1) as MSSubAlgebra of U2 by A1, MSUALG_2:def 17;

      reconsider G = ( GenMSAlg B2) as MSSubAlgebra of U1 by MSUALG_2: 6;

      B1 is MSSubset of G by A1, MSUALG_2:def 17;

      then

       A2: ( GenMSAlg B1) is MSSubAlgebra of G by MSUALG_2:def 17;

      B1 is MSSubset of H by MSUALG_2:def 17;

      then ( GenMSAlg B2) is MSSubAlgebra of ( GenMSAlg B1) by A1, MSUALG_2:def 17;

      hence thesis by A2, MSUALG_2: 7;

    end;

    theorem :: EXTENS_1:19

    for U1 be non-empty MSAlgebra over S holds for U2 be non-empty MSAlgebra over S holds for Gen be GeneratorSet of U1 holds for h1,h2 be 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 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);

      defpred P[ object, object] means ex s be SortSymbol of S st $1 = s & ((h1 . s) . $2) = ((h2 . s) . $2);

      set I = the carrier of S;

      consider A be ManySortedSet of I such that

       A4: for i be object st i in I holds for e be object holds e in (A . i) iff e in (the Sorts of U1 . i) & P[i, e] from PBOOLE:sch 2;

      A is ManySortedSubset of the Sorts of U1

      proof

        let i be object such that

         A5: i in I;

        let e be object;

        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 object;

        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 be object 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 3;

        

         A8: x in (((A # ) * the Arity of S) . o) by A6, RELAT_1: 57;

        then x in ((A # ) . (the Arity of S . o)) by FUNCT_2: 15;

        then x in ((A # ) . ar) by MSUALG_1:def 1;

        then

         A9: x in ( product (A * ar)) by FINSEQ_2:def 5;

        reconsider x as Element of ( Args (o,U1)) by A6;

        

         A10: y = (( Den (o,U1)) . x) by A7, A8, FUNCT_1: 49;

        

         A11: ( dom (h1 # x)) = ( dom ar) by MSUALG_3: 6;

        

         A12: for n be object st n in ( dom (h1 # x)) holds ((h1 # x) . n) = ((h2 # x) . n)

        proof

          let n be object;

          

           A13: ( dom x) = ( dom ar) by MSUALG_3: 6;

          assume

           A14: n in ( dom (h1 # x));

          then

          reconsider n9 = n as Nat by A11, ORDINAL1:def 12;

          ( dom x) = ( dom (A * ar)) by A9, CARD_3: 9;

          then (x . n) in ((A * ar) . n) by A9, A11, A14, A13, CARD_3: 9;

          then (x . n) in (A . (ar . n)) by A11, A14, FUNCT_1: 13;

          then (x . n) in (A . (ar /. n)) by A11, A14, PARTFUN1:def 6;

          then ex s be 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 . n9)) by A11, A14, A13, MSUALG_3:def 6

          .= ((h2 # x) . n) by A11, A14, A13, MSUALG_3:def 6;

        end;

        (( Den (o,U1)) . x) is Element of ((the Sorts of U1 * the ResultSort of S) . o) by MSUALG_1:def 5;

        then (( Den (o,U1)) . x) is Element of (the Sorts of U1 . (the ResultSort of S . o)) by FUNCT_2: 15;

        then

         A15: (( Den (o,U1)) . x) is Element of (the Sorts of U1 . r) by MSUALG_1:def 2;

        

         A16: ( dom (h2 # x)) = ( dom ar) by MSUALG_3: 6;

        ((h1 . r) . y) = ((h1 . r) . (( Den (o,U1)) . x)) by A7, A8, FUNCT_1: 49

        .= (( Den (o,U2)) . (h1 # x)) by A1

        .= (( Den (o,U2)) . (h2 # x)) by A16, A12, FUNCT_1: 2, MSUALG_3: 6

        .= ((h2 . r) . (( Den (o,U1)) . x)) by A2

        .= ((h2 . r) . y) by A7, A8, FUNCT_1: 49;

        then y in (A . r) by A4, A10, A15;

        then y in (A . (the ResultSort of S . o)) by MSUALG_1:def 2;

        hence thesis by FUNCT_2: 15;

      end;

      then

       A17: (U1 | A) = MSAlgebra (# A, ( Opers (U1,A)) #) by MSUALG_2:def 15;

      Gen is ManySortedSubset of the Sorts of (U1 | A)

      proof

        let i be object such that

         A18: i in I;

        reconsider s = i as SortSymbol of S by A18;

        Gen c= the Sorts of U1 by PBOOLE:def 18;

        then

         A19: (Gen . i) c= (the Sorts of U1 . i) by A18;

        let x be object such that

         A20: x in (Gen . i);

        ((h1 . s) . x) = (((h1 . s) | (Gen . s)) . x) by A20, FUNCT_1: 49

        .= (((h1 || Gen) . s) . x) by MSAFREE:def 1

        .= (((h2 . s) | (Gen . s)) . x) by A3, MSAFREE:def 1

        .= ((h2 . s) . x) by A20, FUNCT_1: 49;

        hence thesis by A4, A17, A20, A19;

      end;

      then

       A21: ( GenMSAlg Gen) is MSSubAlgebra of (U1 | A) by MSUALG_2:def 17;

      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 9;

      then

       A22: the Sorts of U1 c= A by PBOOLE:def 18;

      now

        let i be object;

        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:

        now

          

           A26: (the Sorts of U1 . i) c= (A . i) by A22, A23;

          let x be object;

          assume x in ( dom (h1 . s));

          then ex t be SortSymbol of S st t = s & ((h1 . t) . x) = ((h2 . t) . x) by A4, A24, A26;

          hence ((h1 . s) . x) = ((h2 . s) . x);

        end;

        ( dom (h2 . s)) = (the Sorts of U1 . i) by FUNCT_2:def 1;

        hence (h1 . i) = (h2 . i) by A24, A25, FUNCT_1: 2;

      end;

      hence thesis;

    end;