osalg_3.miz



    begin

    reserve R for non empty Poset,

S1 for OrderSortedSign;

    definition

      let R;

      let F be ManySortedFunction of the carrier of R;

      :: OSALG_3:def1

      attr F is order-sorted means for s1,s2 be Element of R st s1 <= s2 holds for a1 be set st a1 in ( dom (F . s1)) holds a1 in ( dom (F . s2)) & ((F . s1) . a1) = ((F . s2) . a1);

    end

    theorem :: OSALG_3:1

    

     Th1: for F be ManySortedFunction of the carrier of R st F is order-sorted holds for s1,s2 be Element of R st s1 <= s2 holds ( dom (F . s1)) c= ( dom (F . s2)) & (F . s1) c= (F . s2)

    proof

      let F be ManySortedFunction of the carrier of R such that

       A1: F is order-sorted;

      let s1,s2 be Element of R such that

       A2: s1 <= s2;

      thus ( dom (F . s1)) c= ( dom (F . s2)) by A1, A2;

      for a,b be object holds [a, b] in (F . s1) implies [a, b] in (F . s2)

      proof

        let y,z be object such that

         A3: [y, z] in (F . s1);

        y in ( dom (F . s1)) by A3, XTUPLE_0:def 12;

        then

         A4: y in ( dom (F . s2)) & ((F . s1) . y) = ((F . s2) . y) by A1, A2;

        ((F . s1) . y) = z by A3, FUNCT_1: 1;

        hence thesis by A4, FUNCT_1: 1;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    theorem :: OSALG_3:2

    

     Th2: for A be OrderSortedSet of R, B be non-empty OrderSortedSet of R, F be ManySortedFunction of A, B holds F is order-sorted iff for s1,s2 be Element of R st s1 <= s2 holds for a1 be set st a1 in (A . s1) holds ((F . s1) . a1) = ((F . s2) . a1)

    proof

      let A be OrderSortedSet of R, B be non-empty OrderSortedSet of R, F be ManySortedFunction of A, B;

      hereby

        assume

         A1: F is order-sorted;

        let s1,s2 be Element of R such that

         A2: s1 <= s2;

        let a1 be set;

        assume a1 in (A . s1);

        then a1 in ( dom (F . s1)) by FUNCT_2:def 1;

        hence ((F . s1) . a1) = ((F . s2) . a1) by A1, A2;

      end;

      assume

       A3: for s1,s2 be Element of R st s1 <= s2 holds for a1 be set st a1 in (A . s1) holds ((F . s1) . a1) = ((F . s2) . a1);

      let s1,s2 be Element of R such that

       A4: s1 <= s2;

      

       A5: ( dom (F . s1)) = (A . s1) & ( dom (F . s2)) = (A . s2) by FUNCT_2:def 1;

      let a1 be set such that

       A6: a1 in ( dom (F . s1));

      (A . s1) c= (A . s2) by A4, OSALG_1:def 16;

      hence a1 in ( dom (F . s2)) by A6, A5;

      thus ((F . s1) . a1) = ((F . s2) . a1) by A3, A4, A6;

    end;

    theorem :: OSALG_3:3

    for F be ManySortedFunction of the carrier of R st F is order-sorted holds for w1,w2 be Element of (the carrier of R * ) st w1 <= w2 holds ((F # ) . w1) c= ((F # ) . w2)

    proof

      let F be ManySortedFunction of the carrier of R such that

       A1: F is order-sorted;

      let w1,w2 be Element of (the carrier of R * ) such that

       A2: w1 <= w2;

      

       A3: ( len w1) = ( len w2) by A2;

      then

       A4: ( dom w1) = ( dom w2) by FINSEQ_3: 29;

      thus ((F # ) . w1) c= ((F # ) . w2)

      proof

        set a = ((F # ) . w1), b = ((F # ) . w2);

        

         A5: a = ( product (F * w1)) by FINSEQ_2:def 5;

        let x be object;

        assume x in ((F # ) . w1);

        then

        consider g be Function such that

         A6: x = g & ( dom g) = ( dom (F * w1)) and

         A7: for y be object st y in ( dom (F * w1)) holds (g . y) in ((F * w1) . y) by A5, CARD_3:def 5;

        

         A8: ( dom F) = the carrier of R by PARTFUN1:def 2;

        ( rng w2) c= the carrier of R;

        then

         A9: ( dom (F * w2)) = ( dom w2) by A8, RELAT_1: 27;

        ( rng w1) c= the carrier of R;

        then

         A10: ( dom (F * w1)) = ( dom w1) by A8, RELAT_1: 27;

        

         A11: for z be object st z in ( dom (F * w2)) holds (g . z) in ((F * w2) . z)

        proof

          let z be object such that

           A12: z in ( dom (F * w2));

          

           A13: ((F * w2) . z) = (F . (w2 . z)) by A12, FUNCT_1: 12;

          (w1 . z) in ( rng w1) & (w2 . z) in ( rng w2) by A4, A9, A12, FUNCT_1: 3;

          then

          reconsider s1 = (w1 . z), s2 = (w2 . z) as Element of R;

          z in ( dom (F * w1)) by A3, A10, A9, A12, FINSEQ_3: 29;

          then s1 <= s2 by A2, A10;

          then

           A14: (F . s1) c= (F . s2) by A1, Th1;

          (g . z) in ((F * w1) . z) & ((F * w1) . z) = (F . (w1 . z)) by A4, A7, A10, A9, A12, FUNCT_1: 12;

          hence thesis by A13, A14;

        end;

        b = ( product (F * w2)) by FINSEQ_2:def 5;

        hence thesis by A4, A6, A10, A9, A11, CARD_3:def 5;

      end;

    end;

    theorem :: OSALG_3:4

    

     Th4: for A be OrderSortedSet of R holds ( id A) is order-sorted

    proof

      let A be OrderSortedSet of R;

      set F = ( id A);

      let s1,s2 be Element of R;

      assume s1 <= s2;

      then

       A1: (A . s1) c= (A . s2) by OSALG_1:def 16;

      let a1 be set such that

       A2: a1 in ( dom (F . s1));

      (A . s2) = {} implies (A . s2) = {} ;

      then ( dom (F . s2)) = (A . s2) by FUNCT_2:def 1;

      hence a1 in ( dom (F . s2)) by A2, A1;

      ((F . s1) . a1) = (( id (A . s1)) . a1) by MSUALG_3:def 1

      .= a1 by A2, FUNCT_1: 18

      .= (( id (A . s2)) . a1) by A2, A1, FUNCT_1: 18

      .= ((F . s2) . a1) by MSUALG_3:def 1;

      hence thesis;

    end;

    registration

      let R;

      let A be OrderSortedSet of R;

      cluster ( id A) -> order-sorted;

      coherence by Th4;

    end

    theorem :: OSALG_3:5

    

     Th5: for A be OrderSortedSet of R holds for B,C be non-empty OrderSortedSet of R, F be ManySortedFunction of A, B, G be ManySortedFunction of B, C holds F is order-sorted & G is order-sorted implies (G ** F) is order-sorted

    proof

      let A be OrderSortedSet of R, B,C be non-empty OrderSortedSet of R, F be ManySortedFunction of A, B, G be ManySortedFunction of B, C;

      assume that

       A1: F is order-sorted and

       A2: G is order-sorted;

      for s1,s2 be Element of R st s1 <= s2 holds for a1 be set st a1 in (A . s1) holds (((G ** F) . s1) . a1) = (((G ** F) . s2) . a1)

      proof

        let s1,s2 be Element of R such that

         A3: s1 <= s2;

        

         A4: (A . s1) c= (A . s2) by A3, OSALG_1:def 16;

        let a1 be set such that

         A5: a1 in (A . s1);

        

         A6: ((F . s1) . a1) = ((F . s2) . a1) by A1, A3, A5, Th2;

        ((F . s1) . a1) in (B . s1) by A5, FUNCT_2: 5;

        then

         A7: ((G . s1) . ((F . s2) . a1)) = ((G . s2) . ((F . s2) . a1)) by A2, A3, A6, Th2;

        (((G ** F) . s1) . a1) = (((G . s1) * (F . s1)) . a1) by MSUALG_3: 2

        .= ((G . s1) . ((F . s2) . a1)) by A5, A6, FUNCT_2: 15

        .= (((G . s2) * (F . s2)) . a1) by A5, A4, A7, FUNCT_2: 15

        .= (((G ** F) . s2) . a1) by MSUALG_3: 2;

        hence thesis;

      end;

      hence thesis by Th2;

    end;

    theorem :: OSALG_3:6

    

     Th6: for A,B be OrderSortedSet of R, F be ManySortedFunction of A, B st F is "1-1" & F is "onto" & F is order-sorted holds (F "" ) is order-sorted

    proof

      let A,B be OrderSortedSet of R;

      let F be ManySortedFunction of A, B such that

       A1: F is "1-1" and

       A2: F is "onto" and

       A3: F is order-sorted;

      let s1,s2 be Element of R such that

       A4: s1 <= s2;

      

       A5: (B . s1) c= (B . s2) by A4, OSALG_1:def 16;

      

       A6: ((F "" ) . s2) = ((F . s2) " ) by A1, A2, MSUALG_3:def 4;

      

       A7: (A . s1) c= (A . s2) by A4, OSALG_1:def 16;

      s1 in the carrier of R;

      then s1 in ( dom F) by PARTFUN1:def 2;

      then

       A8: (F . s1) is one-to-one by A1, MSUALG_3:def 2;

      s2 in the carrier of R;

      then s2 in ( dom F) by PARTFUN1:def 2;

      then

       A9: (F . s2) is one-to-one by A1, MSUALG_3:def 2;

      let a1 be set such that

       A10: a1 in ( dom ((F "" ) . s1));

      

       A11: a1 in (B . s1) by A10;

      then

       A12: ( dom (F . s2)) = (A . s2) by A5, FUNCT_2:def 1;

      set c1 = (((F . s1) " ) . a1), c2 = (((F . s2) " ) . a1);

      

       A13: ( dom (F . s1)) = (A . s1) by A10, FUNCT_2:def 1;

      

       A14: ((F "" ) . s1) = ((F . s1) " ) by A1, A2, MSUALG_3:def 4;

      then

       A15: (((F . s1) " ) . a1) in ( rng ((F . s1) " )) by A10, FUNCT_1: 3;

      

       A16: ( rng (F . s1)) = (B . s1) by A2, MSUALG_3:def 3;

      then ((F . s1) " ) is Function of (B . s1), (A . s1) by A8, FUNCT_2: 25;

      then

       A17: ( rng ((F . s1) " )) c= (A . s1) by RELAT_1:def 19;

      then

       A18: (((F . s1) " ) . a1) in (A . s1) by A15;

      

       A19: ( rng (F . s2)) = (B . s2) by A2, MSUALG_3:def 3;

      

      then

       A20: ((F . s2) . c2) = a1 by A5, A9, A11, FUNCT_1: 35

      .= ((F . s1) . c1) by A10, A16, A8, FUNCT_1: 35

      .= ((F . s2) . c1) by A3, A4, A15, A17, A13;

      a1 in (B . s2) by A5, A11;

      hence a1 in ( dom ((F "" ) . s2)) by A7, A18, FUNCT_2:def 1;

      ((F . s2) " ) is Function of (B . s2), (A . s2) by A19, A9, FUNCT_2: 25;

      then c2 in ( dom (F . s2)) by A5, A7, A11, A18, A12, FUNCT_2: 5;

      hence thesis by A7, A9, A14, A6, A18, A12, A20, FUNCT_1:def 4;

    end;

    theorem :: OSALG_3:7

    

     Th7: for A be OrderSortedSet of R, F be ManySortedFunction of the carrier of R st F is order-sorted holds (F .:.: A) is OrderSortedSet of R

    proof

      let A be OrderSortedSet of R;

      let F be ManySortedFunction of the carrier of R such that

       A1: F is order-sorted;

      reconsider C1 = (F .:.: A) as ManySortedSet of R;

      C1 is order-sorted

      proof

        let s1,s2 be Element of R;

        assume s1 <= s2;

        then

         A2: (A . s1) c= (A . s2) & (F . s1) c= (F . s2) by A1, Th1, OSALG_1:def 16;

        (C1 . s1) = ((F . s1) .: (A . s1)) & (C1 . s2) = ((F . s2) .: (A . s2)) by PBOOLE:def 20;

        hence thesis by A2, RELAT_1: 125;

      end;

      hence thesis;

    end;

    definition

      let S1;

      let U1,U2 be OSAlgebra of S1;

      :: OSALG_3:def2

      pred U1,U2 are_os_isomorphic means ex F be ManySortedFunction of U1, U2 st F is_isomorphism (U1,U2) & F is order-sorted;

    end

    theorem :: OSALG_3:8

    

     Th8: for U1 be OSAlgebra of S1 holds (U1,U1) are_os_isomorphic

    proof

      let U1 be OSAlgebra of S1;

      take ( id the Sorts of U1);

      the Sorts of U1 is OrderSortedSet of S1 by OSALG_1: 17;

      hence thesis by MSUALG_3: 16;

    end;

    theorem :: OSALG_3:9

    

     Th9: for U1,U2 be non-empty OSAlgebra of S1 holds (U1,U2) are_os_isomorphic implies (U2,U1) are_os_isomorphic

    proof

      let U1,U2 be non-empty OSAlgebra of S1;

      

       A1: the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is OrderSortedSet of S1 by OSALG_1: 17;

      assume (U1,U2) are_os_isomorphic ;

      then

      consider F be ManySortedFunction of U1, U2 such that

       A2: F is_isomorphism (U1,U2) and

       A3: F is order-sorted;

      reconsider G = (F "" ) as ManySortedFunction of U2, U1;

      

       A4: G is_isomorphism (U2,U1) by A2, MSUALG_3: 14;

      F is "onto" & F is "1-1" by A2, MSUALG_3: 13;

      then (F "" ) is order-sorted by A3, A1, Th6;

      hence thesis by A4;

    end;

    definition

      let S1;

      let U1,U2 be OSAlgebra of S1;

      :: original: are_os_isomorphic

      redefine

      pred U1,U2 are_os_isomorphic ;

      reflexivity by Th8;

    end

    definition

      let S1;

      let U1,U2 be non-empty OSAlgebra of S1;

      :: original: are_os_isomorphic

      redefine

      pred U1,U2 are_os_isomorphic ;

      symmetry by Th9;

    end

    theorem :: OSALG_3:10

    for U1,U2,U3 be non-empty OSAlgebra of S1 holds (U1,U2) are_os_isomorphic & (U2,U3) are_os_isomorphic implies (U1,U3) are_os_isomorphic

    proof

      let U1,U2,U3 be non-empty OSAlgebra of S1;

      assume that

       A1: (U1,U2) are_os_isomorphic and

       A2: (U2,U3) are_os_isomorphic ;

      consider F be ManySortedFunction of U1, U2 such that

       A3: F is_isomorphism (U1,U2) and

       A4: F is order-sorted by A1;

      consider G be ManySortedFunction of U2, U3 such that

       A5: G is_isomorphism (U2,U3) and

       A6: G is order-sorted by A2;

      reconsider H = (G ** F) as ManySortedFunction of U1, U3;

      

       A7: H is_isomorphism (U1,U3) by A3, A5, MSUALG_3: 15;

      

       A8: the Sorts of U3 is non-empty OrderSortedSet of S1 by OSALG_1: 17;

      the Sorts of U1 is non-empty OrderSortedSet of S1 & the Sorts of U2 is non-empty OrderSortedSet of S1 by OSALG_1: 17;

      then H is order-sorted by A4, A6, A8, Th5;

      hence thesis by A7;

    end;

    theorem :: OSALG_3:11

    

     Th11: for U1,U2 be non-empty OSAlgebra of S1 holds for F be ManySortedFunction of U1, U2 st F is order-sorted & F is_homomorphism (U1,U2) holds ( Image F) is order-sorted

    proof

      let U1,U2 be non-empty OSAlgebra of S1;

      let F be ManySortedFunction of U1, U2 such that

       A1: F is order-sorted and

       A2: F is_homomorphism (U1,U2);

      reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1: 17;

      (F .:.: O1) is OrderSortedSet of S1 by A1, Th7;

      then the Sorts of ( Image F) is OrderSortedSet of S1 by A2, MSUALG_3:def 12;

      hence thesis by OSALG_1: 17;

    end;

    theorem :: OSALG_3:12

    

     Th12: for U1,U2 be non-empty OSAlgebra of S1 holds for F be ManySortedFunction of U1, U2 st F is order-sorted holds for o1,o2 be OperSymbol of S1 st o1 <= o2 holds for x be Element of ( Args (o1,U1)), x1 be Element of ( Args (o2,U1)) st x = x1 holds (F # x) = (F # x1)

    proof

      let U1,U2 be non-empty OSAlgebra of S1;

      let F be ManySortedFunction of U1, U2 such that

       A1: F is order-sorted;

      let o1,o2 be OperSymbol of S1 such that

       A2: o1 <= o2;

      let x be Element of ( Args (o1,U1)), x1 be Element of ( Args (o2,U1)) such that

       A3: x = x1;

      

       A4: ( dom x) = ( dom ( the_arity_of o1)) by MSUALG_3: 6;

      

       A5: for n be object st n in ( dom x) holds ((F # x) . n) = ((F # x1) . n)

      proof

        let n1 be object such that

         A6: n1 in ( dom x);

        reconsider n2 = n1 as Nat by A6, ORDINAL1:def 12;

        reconsider pi1 = (( the_arity_of o1) /. n2), pi2 = (( the_arity_of o2) /. n2) as Element of S1;

        

         A7: (( the_arity_of o1) /. n2) = (( the_arity_of o1) . n2) by A4, A6, PARTFUN1:def 6;

        

         A8: ( the_arity_of o1) <= ( the_arity_of o2) by A2;

        then ( len ( the_arity_of o1)) = ( len ( the_arity_of o2));

        then ( dom ( the_arity_of o1)) = ( dom ( the_arity_of o2)) by FINSEQ_3: 29;

        then (( the_arity_of o2) /. n2) = (( the_arity_of o2) . n2) by A4, A6, PARTFUN1:def 6;

        then

         A9: pi1 <= pi2 by A4, A6, A8, A7;

        ( rng ( the_arity_of o1)) c= the carrier of S1;

        then ( rng ( the_arity_of o1)) c= ( dom the Sorts of U1) by PARTFUN1:def 2;

        then

         A10: n2 in ( dom (the Sorts of U1 * ( the_arity_of o1))) by A4, A6, RELAT_1: 27;

        ( dom (F . pi1)) = (the Sorts of U1 . pi1) by FUNCT_2:def 1

        .= (the Sorts of U1 . (( the_arity_of o1) . n2)) by A4, A6, PARTFUN1:def 6

        .= ((the Sorts of U1 * ( the_arity_of o1)) . n2) by A4, A6, FUNCT_1: 13;

        then

         A11: (x1 . n2) in ( dom (F . pi1)) by A3, A10, MSUALG_3: 6;

        ((F # x) . n2) = ((F . (( the_arity_of o1) /. n2)) . (x1 . n2)) by A3, A6, MSUALG_3:def 6

        .= ((F . pi2) . (x1 . n2)) by A1, A11, A9

        .= ((F # x1) . n2) by A3, A6, MSUALG_3:def 6;

        hence thesis;

      end;

      ( dom x1) = ( dom ( the_arity_of o2)) by MSUALG_3: 6;

      then

       A12: ( dom (F # x1)) = ( dom x1) by MSUALG_3: 6;

      ( dom (F # x)) = ( dom x) by A4, MSUALG_3: 6;

      hence thesis by A3, A12, A5, FUNCT_1: 2;

    end;

    theorem :: OSALG_3:13

    

     Th13: for U1 be monotone non-empty OSAlgebra of S1, U2 be non-empty OSAlgebra of S1 holds for F be ManySortedFunction of U1, U2 st F is order-sorted & F is_homomorphism (U1,U2) holds ( Image F) is order-sorted & ( Image F) is monotone OSAlgebra of S1

    proof

      let U1 be monotone non-empty OSAlgebra of S1, U2 be non-empty OSAlgebra of S1;

      let F be ManySortedFunction of U1, U2 such that

       A1: F is order-sorted and

       A2: F is_homomorphism (U1,U2);

      reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1: 17;

      (F .:.: O1) is OrderSortedSet of S1 by A1, Th7;

      then

       A3: the Sorts of ( Image F) is OrderSortedSet of S1 by A2, MSUALG_3:def 12;

      then

      reconsider I = ( Image F) as non-empty OSAlgebra of S1 by OSALG_1: 17;

      thus ( Image F) is order-sorted by A3, OSALG_1: 17;

      consider G be ManySortedFunction of U1, I such that

       A4: F = G and

       A5: G is_epimorphism (U1,I) by A2, MSUALG_3: 21;

      

       A6: G is_homomorphism (U1,I) by A5, MSUALG_3:def 8;

      

       A7: G is "onto" by A5, MSUALG_3:def 8;

      for o1,o2 be OperSymbol of S1 st o1 <= o2 holds ( Den (o1,I)) c= ( Den (o2,I))

      proof

        let o1,o2 be OperSymbol of S1 such that

         A8: o1 <= o2;

        

         A9: ( Args (o1,I)) c= ( Args (o2,I)) by A8, OSALG_1: 26;

        

         A10: ( Args (o1,U1)) c= ( Args (o2,U1)) by A8, OSALG_1: 26;

        

         A11: ( dom ( Den (o2,I))) = ( Args (o2,I)) by FUNCT_2:def 1;

        

         A12: (( Den (o2,U1)) | ( Args (o1,U1))) = ( Den (o1,U1)) by A8, OSALG_1:def 21;

        

         A13: ( the_result_sort_of o1) <= ( the_result_sort_of o2) by A8;

        for a,b be object holds [a, b] in ( Den (o1,I)) implies [a, b] in ( Den (o2,I))

        proof

          set s1 = ( the_result_sort_of o1), s2 = ( the_result_sort_of o2);

          o1 in the carrier' of S1;

          then

           A14: o1 in ( dom the ResultSort of S1) by FUNCT_2:def 1;

          let a,b be object such that

           A15: [a, b] in ( Den (o1,I));

          

           A16: a in ( Args (o1,I)) by A15, ZFMISC_1: 87;

          then

          consider y be Element of ( Args (o1,U1)) such that

           A17: (G # y) = a by A7, MSUALG_9: 17;

          reconsider y1 = y as Element of ( Args (o2,U1)) by A10;

          

           A18: (G # y1) = (G # y) & (( Den (o2,U1)) . y) = (( Den (o1,U1)) . y) by A1, A4, A8, A12, Th12, FUNCT_1: 49;

          set x = (( Den (o1,U1)) . y);

          ((G . s1) . x) = (( Den (o1,I)) . a) by A6, A17, MSUALG_3:def 7;

          then

           A19: b = ((G . s1) . x) by A15, FUNCT_1: 1;

          ( Result (o1,U1)) = ((O1 * the ResultSort of S1) . o1) by MSUALG_1:def 5

          .= (O1 . (the ResultSort of S1 . o1)) by A14, FUNCT_1: 13

          .= (O1 . s1) by MSUALG_1:def 2

          .= ( dom (G . s1)) by FUNCT_2:def 1;

          then ((G . s1) . x) = ((G . s2) . x) by A1, A4, A13;

          then b = (( Den (o2,I)) . a) by A6, A17, A19, A18, MSUALG_3:def 7;

          hence thesis by A9, A11, A16, FUNCT_1: 1;

        end;

        hence thesis by RELAT_1:def 3;

      end;

      hence thesis by OSALG_1: 27;

    end;

    theorem :: OSALG_3:14

    

     Th14: for U1 be monotone OSAlgebra of S1, U2 be OSSubAlgebra of U1 holds U2 is monotone

    proof

      let U1 be monotone OSAlgebra of S1, U2 be OSSubAlgebra of U1;

      let o1,o2 be OperSymbol of S1 such that

       A1: o1 <= o2;

      

       A2: ( Args (o1,U2)) c= ( Args (o2,U2)) by A1, OSALG_1: 26;

      the Sorts of U2 is MSSubset of U1 & the Sorts of U2 is OrderSortedSet of S1 by MSUALG_2:def 9, OSALG_1: 17;

      then

      reconsider B = the Sorts of U2 as OSSubset of U1 by OSALG_2:def 2;

      

       A3: B is opers_closed by MSUALG_2:def 9;

      then

       A4: B is_closed_on o1 by MSUALG_2:def 6;

      

       A5: B is_closed_on o2 by A3, MSUALG_2:def 6;

      

       A6: ( Den (o2,U2)) = (the Charact of U2 . o2) by MSUALG_1:def 6

      .= (( Opers (U1,B)) . o2) by MSUALG_2:def 9

      .= (o2 /. B) by MSUALG_2:def 8

      .= (( Den (o2,U1)) | (((B # ) * the Arity of S1) . o2)) by A5, MSUALG_2:def 7

      .= (( Den (o2,U1)) | ( Args (o2,U2))) by MSUALG_1:def 4;

      

       A7: ( Den (o1,U2)) = (the Charact of U2 . o1) by MSUALG_1:def 6

      .= (( Opers (U1,B)) . o1) by MSUALG_2:def 9

      .= (o1 /. B) by MSUALG_2:def 8

      .= (( Den (o1,U1)) | (((B # ) * the Arity of S1) . o1)) by A4, MSUALG_2:def 7

      .= (( Den (o1,U1)) | ( Args (o1,U2))) by MSUALG_1:def 4;

      (( Den (o2,U1)) | ( Args (o1,U1))) = ( Den (o1,U1)) by A1, OSALG_1:def 21;

      

      then ( Den (o1,U2)) = (( Den (o2,U1)) | (( Args (o1,U1)) /\ ( Args (o1,U2)))) by A7, RELAT_1: 71

      .= (( Den (o2,U1)) | ( Args (o1,U2))) by MSAFREE3: 37, XBOOLE_1: 28

      .= (( Den (o2,U1)) | (( Args (o2,U2)) /\ ( Args (o1,U2)))) by A2, XBOOLE_1: 28

      .= (( Den (o2,U2)) | ( Args (o1,U2))) by A6, RELAT_1: 71;

      hence thesis;

    end;

    registration

      let S1;

      let U1 be monotone OSAlgebra of S1;

      cluster monotone for OSSubAlgebra of U1;

      existence

      proof

        set U2 = the OSSubAlgebra of U1;

        take U2;

        thus thesis by Th14;

      end;

    end

    registration

      let S1;

      let U1 be monotone OSAlgebra of S1;

      cluster -> monotone for OSSubAlgebra of U1;

      coherence by Th14;

    end

    theorem :: OSALG_3:15

    

     Th15: for U1,U2 be non-empty OSAlgebra of S1 holds for F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) & F is order-sorted holds ex G be ManySortedFunction of U1, ( Image F) st F = G & G is order-sorted & G is_epimorphism (U1,( Image F))

    proof

      let U1,U2 be non-empty OSAlgebra of S1;

      let F be ManySortedFunction of U1, U2;

      assume that

       A1: F is_homomorphism (U1,U2) and

       A2: F is order-sorted;

      consider G be ManySortedFunction of U1, ( Image F) such that

       A3: F = G & G is_epimorphism (U1,( Image F)) by A1, MSUALG_3: 21;

      take G;

      thus thesis by A2, A3;

    end;

    theorem :: OSALG_3:16

    for U1,U2 be non-empty OSAlgebra of S1 holds for F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) & F is order-sorted holds ex F1 be ManySortedFunction of U1, ( Image F), F2 be ManySortedFunction of ( Image F), U2 st F1 is_epimorphism (U1,( Image F)) & F2 is_monomorphism (( Image F),U2) & F = (F2 ** F1) & F1 is order-sorted & F2 is order-sorted

    proof

      let U1,U2 be non-empty OSAlgebra of S1;

      let F be ManySortedFunction of U1, U2;

      assume that

       A1: F is_homomorphism (U1,U2) and

       A2: F is order-sorted;

      for H be ManySortedFunction of ( Image F), ( Image F) holds H is ManySortedFunction of ( Image F), U2

      proof

        let H be ManySortedFunction of ( Image F), ( Image F);

        for i be object st i in the carrier of S1 holds (H . i) is Function of (the Sorts of ( Image F) . i), (the Sorts of U2 . i)

        proof

          let i be object;

          assume

           A3: i in the carrier of S1;

          then

          reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

          reconsider h = (H . i) as Function of (the Sorts of ( Image F) . i), (the Sorts of ( Image F) . i) by A3, PBOOLE:def 15;

          

           A4: ( dom f) = (the Sorts of U1 . i) by A3, FUNCT_2:def 1;

          the Sorts of ( Image F) = (F .:.: the Sorts of U1) by A1, MSUALG_3:def 12;

          

          then (the Sorts of ( Image F) . i) = (f .: (the Sorts of U1 . i)) by A3, PBOOLE:def 20

          .= ( rng f) by A4, RELAT_1: 113;

          then h is Function of (the Sorts of ( Image F) . i), (the Sorts of U2 . i) by FUNCT_2: 7;

          hence thesis;

        end;

        hence thesis by PBOOLE:def 15;

      end;

      then

      reconsider F2 = ( id the Sorts of ( Image F)) as ManySortedFunction of ( Image F), U2;

      consider F1 be ManySortedFunction of U1, ( Image F) such that

       A5: F1 = F & F1 is order-sorted and

       A6: F1 is_epimorphism (U1,( Image F)) by A1, A2, Th15;

      take F1, F2;

      thus F1 is_epimorphism (U1,( Image F)) by A6;

      thus F2 is_monomorphism (( Image F),U2) by MSUALG_3: 22;

      thus F = (F2 ** F1) & F1 is order-sorted by A5, MSUALG_3: 4;

      ( Image F) is order-sorted by A1, A2, Th11;

      then the Sorts of ( Image F) is OrderSortedSet of S1 by OSALG_1: 17;

      hence thesis;

    end;

    registration

      let S1;

      let U1 be OSAlgebra of S1;

      cluster MSAlgebra (# the Sorts of U1, the Charact of U1 #) -> order-sorted;

      coherence

      proof

        the Sorts of U1 is OrderSortedSet of S1 by OSALG_1: 17;

        hence thesis by OSALG_1: 17;

      end;

    end

    theorem :: OSALG_3:17

    for U1 be OSAlgebra of S1 holds (U1 is monotone iff MSAlgebra (# the Sorts of U1, the Charact of U1 #) is monotone)

    proof

      let U1 be OSAlgebra of S1;

      set U2 = MSAlgebra (# the Sorts of U1, the Charact of U1 #);

       A1:

      now

        let o1 be OperSymbol of S1;

        

        thus ( Den (o1,U1)) = (the Charact of U2 . o1) by MSUALG_1:def 6

        .= ( Den (o1,U2)) by MSUALG_1:def 6;

        

        thus ( Args (o1,U1)) = (((the Sorts of U2 # ) * the Arity of S1) . o1) by MSUALG_1:def 4

        .= ( Args (o1,U2)) by MSUALG_1:def 4;

      end;

      thus U1 is monotone implies U2 is monotone

      proof

        assume

         A2: U1 is monotone;

        let o1,o2 be OperSymbol of S1;

        assume o1 <= o2;

        then

         A3: (( Den (o2,U1)) | ( Args (o1,U1))) = ( Den (o1,U1)) by A2;

        

        thus (( Den (o2,U2)) | ( Args (o1,U2))) = (( Den (o2,U1)) | ( Args (o1,U2))) by A1

        .= ( Den (o1,U1)) by A1, A3

        .= ( Den (o1,U2)) by A1;

      end;

      assume

       A4: U2 is monotone;

      let o1,o2 be OperSymbol of S1;

      assume o1 <= o2;

      then

       A5: (( Den (o2,U2)) | ( Args (o1,U2))) = ( Den (o1,U2)) by A4;

      

      thus (( Den (o2,U1)) | ( Args (o1,U1))) = (( Den (o2,U2)) | ( Args (o1,U1))) by A1

      .= ( Den (o1,U2)) by A1, A5

      .= ( Den (o1,U1)) by A1;

    end;

    theorem :: OSALG_3:18

    for U1,U2 be strict non-empty OSAlgebra of S1 st (U1,U2) are_os_isomorphic holds U1 is monotone iff U2 is monotone

    proof

      let U1,U2 be strict non-empty OSAlgebra of S1;

      assume (U1,U2) are_os_isomorphic ;

      then

      consider F be ManySortedFunction of U1, U2 such that

       A1: F is_isomorphism (U1,U2) and

       A2: F is order-sorted;

      reconsider O1 = the Sorts of U1, O2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1: 17;

      reconsider F1 = F as ManySortedFunction of O1, O2;

      F is "onto" & F is "1-1" by A1, MSUALG_3: 13;

      then

       A3: (F1 "" ) is order-sorted by A2, Th6;

      

       A4: F is_epimorphism (U1,U2) by A1, MSUALG_3:def 10;

      then

       A5: F is_homomorphism (U1,U2) by MSUALG_3:def 8;

      then ( Image F) = U2 by A4, MSUALG_3: 19;

      hence U1 is monotone implies U2 is monotone by A2, A5, Th13;

      reconsider F2 = (F1 "" ) as ManySortedFunction of U2, U1;

      assume

       A6: U2 is monotone;

      (F "" ) is_isomorphism (U2,U1) by A1, MSUALG_3: 14;

      then

       A7: F2 is_epimorphism (U2,U1) by MSUALG_3:def 10;

      then

       A8: F2 is_homomorphism (U2,U1) by MSUALG_3:def 8;

      then ( Image F2) = U1 by A7, MSUALG_3: 19;

      hence thesis by A3, A8, A6, Th13;

    end;