msualg_4.miz



    begin

    reserve S for non void non empty ManySortedSign,

U1 for MSAlgebra over S,

o for OperSymbol of S,

s for SortSymbol of S;

    registration

      let I be set;

      cluster Relation-yielding for ManySortedSet of I;

      existence

      proof

        set R = the Relation;

        set f = (I --> R);

        reconsider f as ManySortedSet of I;

        take f;

        for x be set st x in ( dom f) holds (f . x) is Relation by FUNCOP_1: 7;

        hence thesis;

      end;

    end

    definition

      let I be set, A,B be ManySortedSet of I;

      :: MSUALG_4:def1

      mode ManySortedRelation of A,B -> ManySortedSet of I means

      : Def1: for i be set st i in I holds (it . i) is Relation of (A . i), (B . i);

      existence

      proof

        consider R be Relation such that

         A1: R = {} ;

        set f = (I --> R);

        reconsider f as ManySortedSet of I;

        take f;

        for i be set st i in I holds (f . i) is Relation of (A . i), (B . i)

        proof

          let i be set;

          assume i in I;

          (f . i) = {} by A1;

          hence thesis by RELSET_1: 12;

        end;

        hence thesis;

      end;

    end

    registration

      let I be set, A,B be ManySortedSet of I;

      cluster -> Relation-yielding for ManySortedRelation of A, B;

      coherence

      proof

        let R be ManySortedRelation of A, B;

        let x be set;

        assume x in ( dom R);

        then x in I;

        hence thesis by Def1;

      end;

    end

    definition

      let I be set, A be ManySortedSet of I;

      mode ManySortedRelation of A is ManySortedRelation of A, A;

    end

    definition

      let I be set, A be ManySortedSet of I;

      let IT be ManySortedRelation of A;

      :: MSUALG_4:def2

      attr IT is MSEquivalence_Relation-like means

      : Def2: for i be set, R be Relation of (A . i) st i in I & (IT . i) = R holds R is Equivalence_Relation of (A . i);

    end

    definition

      let I be non empty set, A,B be ManySortedSet of I, F be ManySortedRelation of A, B, i be Element of I;

      :: original: .

      redefine

      func F . i -> Relation of (A . i), (B . i) ;

      coherence by Def1;

    end

    definition

      let S be non empty ManySortedSign, U1 be MSAlgebra over S;

      mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1;

    end

    definition

      let S be non empty ManySortedSign, U1 be MSAlgebra over S;

      let IT be ManySortedRelation of U1;

      :: MSUALG_4:def3

      attr IT is MSEquivalence-like means

      : Def3: IT is MSEquivalence_Relation-like;

    end

    registration

      let S be non void non empty ManySortedSign, U1 be MSAlgebra over S;

      cluster MSEquivalence-like for ManySortedRelation of U1;

      existence

      proof

        deffunc F( Element of S) = ( id (the Sorts of U1 . $1));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = F(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for i be set st i in the carrier of S holds (f . i) is Relation of (the Sorts of U1 . i), (the Sorts of U1 . i)

        proof

          let i be set;

          assume i in the carrier of S;

          then (f . i) = ( id (the Sorts of U1 . i)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by Def1;

        reconsider f as ManySortedRelation of U1;

        take f;

        for i be set, R be Relation of (the Sorts of U1 . i) st i in the carrier of S & (f . i) = R holds R is Equivalence_Relation of (the Sorts of U1 . i)

        proof

          let i be set, R be Relation of (the Sorts of U1 . i);

          assume i in the carrier of S & (f . i) = R;

          then R = ( id (the Sorts of U1 . i)) by A1;

          hence thesis;

        end;

        then f is MSEquivalence_Relation-like;

        hence thesis;

      end;

    end

    theorem :: MSUALG_4:1

    

     Th1: for R be MSEquivalence-like ManySortedRelation of U1 holds (R . s) is Equivalence_Relation of (the Sorts of U1 . s) by Def3, Def2;

    definition

      let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S, R be MSEquivalence-like ManySortedRelation of U1;

      :: MSUALG_4:def4

      attr R is MSCongruence-like means

      : Def4: for o be OperSymbol of S, x,y be Element of ( Args (o,U1)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (R . (( the_arity_of o) /. n))) holds [(( Den (o,U1)) . x), (( Den (o,U1)) . y)] in (R . ( the_result_sort_of o));

    end

    registration

      let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;

      cluster MSCongruence-like for MSEquivalence-like ManySortedRelation of U1;

      existence

      proof

        deffunc F( Element of S) = ( id (the Sorts of U1 . $1));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = F(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for i be set st i in the carrier of S holds (f . i) is Relation of (the Sorts of U1 . i), (the Sorts of U1 . i)

        proof

          let i be set;

          assume i in the carrier of S;

          then (f . i) = ( id (the Sorts of U1 . i)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by Def1;

        reconsider f as ManySortedRelation of U1;

        for i be set, R be Relation of (the Sorts of U1 . i) st i in the carrier of S & (f . i) = R holds R is Equivalence_Relation of (the Sorts of U1 . i)

        proof

          let i be set, R be Relation of (the Sorts of U1 . i);

          assume i in the carrier of S & (f . i) = R;

          then R = ( id (the Sorts of U1 . i)) by A1;

          hence thesis;

        end;

        then f is MSEquivalence_Relation-like;

        then

        reconsider f as MSEquivalence-like ManySortedRelation of U1 by Def3;

        take f;

        for o be OperSymbol of S, x,y be Element of ( Args (o,U1)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (f . (( the_arity_of o) /. n))) holds [(( Den (o,U1)) . x), (( Den (o,U1)) . y)] in (f . ( the_result_sort_of o))

        proof

          

           A2: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

          then

           A3: ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by PARTFUN1:def 2;

          let o be OperSymbol of S, x,y be Element of ( Args (o,U1));

          

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

          assume

           A5: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (f . (( the_arity_of o) /. n));

          

           A6: for a be object st a in ( dom ( the_arity_of o)) holds (x . a) = (y . a)

          proof

            set ao = ( the_arity_of o);

            let a be object;

            assume

             A7: a in ( dom ( the_arity_of o));

            then

            reconsider n = a as Nat by ORDINAL1:def 12;

            (ao . n) in ( rng ao) by A7, FUNCT_1:def 3;

            then

             A8: (f . (ao . n)) = ( id (the Sorts of U1 . (ao . n))) by A1;

            (( the_arity_of o) /. n) = (( the_arity_of o) . n) by A7, PARTFUN1:def 6;

            then [(x . n), (y . n)] in (f . (ao . n)) by A5, A4, A7;

            hence thesis by A8, RELAT_1:def 10;

          end;

          set r = ( the_result_sort_of o);

          

           A9: (f . r) = ( id (the Sorts of U1 . r)) by A1;

          

           A10: ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) by MSUALG_1:def 5

          .= (the Sorts of U1 . (the ResultSort of S . o)) by A2, A3, FUNCT_1: 12

          .= (the Sorts of U1 . r) by MSUALG_1:def 2;

          ( dom y) = ( dom ( the_arity_of o)) by MSUALG_3: 6;

          then (( Den (o,U1)) . x) = (( Den (o,U1)) . y) by A4, A6, FUNCT_1: 2;

          hence thesis by A9, A10, RELAT_1:def 10;

        end;

        hence thesis;

      end;

    end

    definition

      let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;

      mode MSCongruence of U1 is MSCongruence-like MSEquivalence-like ManySortedRelation of U1;

    end

    definition

      let S be non void non empty ManySortedSign, U1 be MSAlgebra over S, R be MSEquivalence-like ManySortedRelation of U1, i be Element of S;

      :: original: .

      redefine

      func R . i -> Equivalence_Relation of (the Sorts of U1 . i) ;

      coherence by Th1;

    end

    definition

      let S be non void non empty ManySortedSign, U1 be MSAlgebra over S, R be MSEquivalence-like ManySortedRelation of U1, i be Element of S, x be Element of (the Sorts of U1 . i);

      :: MSUALG_4:def5

      func Class (R,x) -> Subset of (the Sorts of U1 . i) equals ( Class ((R . i),x));

      correctness ;

    end

    definition

      let S;

      let U1 be non-empty MSAlgebra over S;

      let R be MSCongruence of U1;

      :: MSUALG_4:def6

      func Class R -> non-empty ManySortedSet of the carrier of S means

      : Def6: for s be Element of S holds (it . s) = ( Class (R . s));

      existence

      proof

        deffunc F( Element of S) = ( Class (R . $1));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = F(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for i be object st i in the carrier of S holds (f . i) is non empty

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          consider x be object such that

           A2: x in (the Sorts of U1 . s) by XBOOLE_0:def 1;

          reconsider y = x as Element of (the Sorts of U1 . s) by A2;

          (f . s) = ( Class (R . s)) by A1;

          then ( Class ((R . s),y)) in (f . s) by EQREL_1:def 3;

          hence thesis;

        end;

        then

        reconsider f as non-empty ManySortedSet of the carrier of S by PBOOLE:def 13;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let C,D be non-empty ManySortedSet of the carrier of S;

        assume that

         A3: for s be Element of S holds (C . s) = ( Class (R . s)) and

         A4: for s be Element of S holds (D . s) = ( Class (R . s));

        now

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          (C . s) = ( Class (R . s)) by A3;

          hence (C . i) = (D . i) by A4;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    begin

    definition

      let S;

      let M1,M2 be ManySortedSet of the carrier' of S;

      let F be ManySortedFunction of M1, M2;

      let o be OperSymbol of S;

      :: original: .

      redefine

      func F . o -> Function of (M1 . o), (M2 . o) ;

      coherence by PBOOLE:def 15;

    end

    registration

      let I be non empty set, p be FinSequence of I, X be ManySortedSet of I;

      cluster (X * p) -> ( dom p) -defined;

      coherence

      proof

        ( rng p) c= I;

        then ( rng p) c= ( dom X) by PARTFUN1:def 2;

        then ( dom (X * p)) = ( dom p) by RELAT_1: 27;

        then

        reconsider Xp = (X * p) as ManySortedSet of ( dom p) by PARTFUN1:def 2, RELAT_1:def 18;

        Xp is ManySortedSet of ( dom p);

        hence thesis;

      end;

    end

    registration

      let I be non empty set, p be FinSequence of I, X be ManySortedSet of I;

      cluster (X * p) -> total;

      coherence

      proof

        ( rng p) c= I;

        then ( rng p) c= ( dom X) by PARTFUN1:def 2;

        then ( dom (X * p)) = ( dom p) by RELAT_1: 27;

        then

        reconsider Xp = (X * p) as ManySortedSet of ( dom p) by PARTFUN1:def 2;

        Xp is ManySortedSet of ( dom p);

        hence thesis;

      end;

    end

    definition

      let S, o;

      let A be non-empty MSAlgebra over S;

      let R be MSCongruence of A;

      let x be Element of ( Args (o,A));

      :: MSUALG_4:def7

      func R # x -> Element of ( product (( Class R) * ( the_arity_of o))) means

      : Def7: for n be Nat st n in ( dom ( the_arity_of o)) holds (it . n) = ( Class ((R . (( the_arity_of o) /. n)),(x . n)));

      existence

      proof

        defpred P[ object, object] means for n be Nat st n = $1 holds $2 = ( Class ((R . (( the_arity_of o) /. n)),(x . n)));

        set ar = ( the_arity_of o), da = ( dom ar);

        

         A1: for y be object st y in da holds ex u be object st P[y, u]

        proof

          let y be object;

          assume y in da;

          then

          reconsider n = y as Nat by ORDINAL1:def 12;

          take ( Class ((R . (( the_arity_of o) /. n)),(x . n)));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = da & for x be object st x in da holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A3: ( dom (( Class R) * ar)) = da by PARTFUN1:def 2;

        for y be object st y in ( dom (( Class R) * ar)) holds (f . y) in ((( Class R) * ar) . y)

        proof

          let y be object;

          assume

           A4: y in ( dom (( Class R) * ar));

          then

          reconsider n = y as Nat by ORDINAL1:def 12;

          (ar . y) in ( rng ar) by A3, A4, FUNCT_1:def 3;

          then

          reconsider s = (ar . y) as Element of S;

          

           A5: y in ( dom (the Sorts of A * ar)) by A3, A4, PARTFUN1:def 2;

          then ((the Sorts of A * ar) . y) = (the Sorts of A . (ar . y)) by FUNCT_1: 12;

          then

           A6: (x . y) in (the Sorts of A . s) by A5, MSUALG_3: 6;

          (f . n) = ( Class ((R . (ar /. n)),(x . n))) & (ar /. n) = (ar . n) by A2, A3, A4, PARTFUN1:def 6;

          then

           A7: (f . y) in ( Class (R . s)) by A6, EQREL_1:def 3;

          ((( Class R) * ar) . y) = (( Class R) . (ar . y)) by A4, FUNCT_1: 12;

          hence thesis by A7, Def6;

        end;

        then

        reconsider f as Element of ( product (( Class R) * ar)) by A2, A3, CARD_3: 9;

        take f;

        let n be Nat;

        assume n in da;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F,G be Element of ( product (( Class R) * ( the_arity_of o)));

        assume that

         A8: for n be Nat st n in ( dom ( the_arity_of o)) holds (F . n) = ( Class ((R . (( the_arity_of o) /. n)),(x . n))) and

         A9: for n be Nat st n in ( dom ( the_arity_of o)) holds (G . n) = ( Class ((R . (( the_arity_of o) /. n)),(x . n)));

        

         A10: for y be object st y in ( dom ( the_arity_of o)) holds (F . y) = (G . y)

        proof

          let y be object;

          assume

           A11: y in ( dom ( the_arity_of o));

          then

          reconsider n = y as Nat by ORDINAL1:def 12;

          (F . n) = ( Class ((R . (( the_arity_of o) /. n)),(x . n))) by A8, A11;

          hence thesis by A9, A11;

        end;

        

         A12: ( dom G) = ( dom ( the_arity_of o)) by PARTFUN1:def 2;

        ( dom F) = ( dom ( the_arity_of o)) by PARTFUN1:def 2;

        hence thesis by A12, A10, FUNCT_1: 2;

      end;

    end

    definition

      let S, o;

      let A be non-empty MSAlgebra over S;

      let R be MSCongruence of A;

      :: MSUALG_4:def8

      func QuotRes (R,o) -> Function of ((the Sorts of A * the ResultSort of S) . o), ((( Class R) * the ResultSort of S) . o) means

      : Def8: for x be Element of (the Sorts of A . ( the_result_sort_of o)) holds (it . x) = ( Class (R,x));

      existence

      proof

        set rs = ( the_result_sort_of o), D = (the Sorts of A . rs);

        deffunc F( Element of D) = ( Class (R,$1));

        consider f be Function such that

         A1: ( dom f) = D & for d be Element of D holds (f . d) = F(d) from FUNCT_1:sch 4;

        

         A2: for x be object st x in D holds (f . x) in (( Class R) . rs)

        proof

          let x be object;

          assume x in D;

          then

          reconsider x1 = x as Element of D;

          (f . x1) = ( Class (R,x1)) by A1;

          then (f . x1) in ( Class (R . rs)) by EQREL_1:def 3;

          hence thesis by Def6;

        end;

        o in the carrier' of S;

        then o in ( dom (the Sorts of A * the ResultSort of S)) by PARTFUN1:def 2;

        

        then

         A3: ((the Sorts of A * the ResultSort of S) . o) = (the Sorts of A . (the ResultSort of S . o)) by FUNCT_1: 12

        .= D by MSUALG_1:def 2;

        

         A4: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

        then ( dom (( Class R) * the ResultSort of S)) = ( dom the ResultSort of S) by PARTFUN1:def 2;

        

        then ((( Class R) * the ResultSort of S) . o) = (( Class R) . (the ResultSort of S . o)) by A4, FUNCT_1: 12

        .= (( Class R) . rs) by MSUALG_1:def 2;

        then

        reconsider f as Function of ((the Sorts of A * the ResultSort of S) . o), ((( Class R) * the ResultSort of S) . o) by A1, A3, A2, FUNCT_2: 3;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set SA = the Sorts of A, RS = the ResultSort of S, rs = ( the_result_sort_of o);

        let f,g be Function of ((the Sorts of A * the ResultSort of S) . o), ((( Class R) * the ResultSort of S) . o);

        assume that

         A5: for x be Element of (SA . rs) holds (f . x) = ( Class (R,x)) and

         A6: for x be Element of (SA . rs) holds (g . x) = ( Class (R,x));

         A7:

        now

          let x be object;

          assume x in (SA . rs);

          then

          reconsider x1 = x as Element of (SA . rs);

          (f . x1) = ( Class (R,x1)) by A5;

          hence (f . x) = (g . x) by A6;

        end;

        o in the carrier' of S;

        then o in ( dom (SA * RS)) by PARTFUN1:def 2;

        

        then ((SA * RS) . o) = (SA . (RS . o)) by FUNCT_1: 12

        .= (SA . rs) by MSUALG_1:def 2;

        then ( dom f) = (SA . rs) & ( dom g) = (SA . rs) by FUNCT_2:def 1;

        hence thesis by A7, FUNCT_1: 2;

      end;

      :: MSUALG_4:def9

      func QuotArgs (R,o) -> Function of (((the Sorts of A # ) * the Arity of S) . o), (((( Class R) # ) * the Arity of S) . o) means for x be Element of ( Args (o,A)) holds (it . x) = (R # x);

      existence

      proof

        set ao = ( the_arity_of o);

        set D = ( Args (o,A));

        deffunc F( Element of D) = (R # $1);

        consider f be Function such that

         A8: ( dom f) = D & for d be Element of D holds (f . d) = F(d) from FUNCT_1:sch 4;

        

         A9: o in the carrier' of S;

        then o in ( dom ((the Sorts of A # ) * the Arity of S)) by PARTFUN1:def 2;

        

        then

         A10: (((the Sorts of A # ) * the Arity of S) . o) = ((the Sorts of A # ) . (the Arity of S . o)) by FUNCT_1: 12

        .= ((the Sorts of A # ) . ( the_arity_of o)) by MSUALG_1:def 1;

        

         A11: for x be object st x in ((the Sorts of A # ) . ao) holds (f . x) in ((( Class R) # ) . ao)

        proof

          let x be object;

          assume x in ((the Sorts of A # ) . ao);

          then

          reconsider x1 = x as Element of D by A10, MSUALG_1:def 4;

          (f . x1) = (R # x1) & ((( Class R) # ) . ao) = ( product (( Class R) * ao)) by A8, FINSEQ_2:def 5;

          hence thesis;

        end;

        o in ( dom ((( Class R) # ) * the Arity of S)) by A9, PARTFUN1:def 2;

        

        then (((( Class R) # ) * the Arity of S) . o) = ((( Class R) # ) . (the Arity of S . o)) by FUNCT_1: 12

        .= ((( Class R) # ) . ao) by MSUALG_1:def 1;

        then

        reconsider f as Function of (((the Sorts of A # ) * the Arity of S) . o), (((( Class R) # ) * the Arity of S) . o) by A8, A10, A11, FUNCT_2: 3, MSUALG_1:def 4;

        take f;

        thus thesis by A8;

      end;

      uniqueness

      proof

        set ao = ( the_arity_of o);

        let f,g be Function of (((the Sorts of A # ) * the Arity of S) . o), (((( Class R) # ) * the Arity of S) . o);

        assume that

         A12: for x be Element of ( Args (o,A)) holds (f . x) = (R # x) and

         A13: for x be Element of ( Args (o,A)) holds (g . x) = (R # x);

        o in the carrier' of S;

        then o in ( dom ((the Sorts of A # ) * the Arity of S)) by PARTFUN1:def 2;

        

        then

         A14: (((the Sorts of A # ) * the Arity of S) . o) = ((the Sorts of A # ) . (the Arity of S . o)) by FUNCT_1: 12

        .= ((the Sorts of A # ) . ( the_arity_of o)) by MSUALG_1:def 1;

         A15:

        now

          let x be object;

          assume x in ((the Sorts of A # ) . ao);

          then

          reconsider x1 = x as Element of ( Args (o,A)) by A14, MSUALG_1:def 4;

          (f . x1) = (R # x1) by A12;

          hence (f . x) = (g . x) by A13;

        end;

        ( dom f) = ((the Sorts of A # ) . ao) & ( dom g) = ((the Sorts of A # ) . ao) by A14, FUNCT_2:def 1;

        hence thesis by A15, FUNCT_1: 2;

      end;

    end

    definition

      let S;

      let A be non-empty MSAlgebra over S;

      let R be MSCongruence of A;

      :: MSUALG_4:def10

      func QuotRes R -> ManySortedFunction of (the Sorts of A * the ResultSort of S), (( Class R) * the ResultSort of S) means for o be OperSymbol of S holds (it . o) = ( QuotRes (R,o));

      existence

      proof

        defpred P[ object, object] means for o be OperSymbol of S st o = $1 holds $2 = ( QuotRes (R,o));

        set O = the carrier' of S;

        

         A1: for x be object st x in O holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in O;

          then

          reconsider x1 = x as OperSymbol of S;

          take ( QuotRes (R,x1));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = O & for x be object st x in O holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        reconsider f as ManySortedSet of O by A2, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x1 = x as OperSymbol of S;

          (f . x1) = ( QuotRes (R,x1)) by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;

        for i be object st i in O holds (f . i) is Function of ((the Sorts of A * the ResultSort of S) . i), ((( Class R) * the ResultSort of S) . i)

        proof

          let i be object;

          assume i in O;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotRes (R,i1)) by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of (the Sorts of A * the ResultSort of S), (( Class R) * the ResultSort of S) by PBOOLE:def 15;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be ManySortedFunction of (the Sorts of A * the ResultSort of S), (( Class R) * the ResultSort of S);

        assume that

         A3: for o be OperSymbol of S holds (f . o) = ( QuotRes (R,o)) and

         A4: for o be OperSymbol of S holds (g . o) = ( QuotRes (R,o));

        now

          let i be object;

          assume i in the carrier' of S;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotRes (R,i1)) by A3;

          hence (f . i) = (g . i) by A4;

        end;

        hence thesis by PBOOLE: 3;

      end;

      :: MSUALG_4:def11

      func QuotArgs R -> ManySortedFunction of ((the Sorts of A # ) * the Arity of S), ((( Class R) # ) * the Arity of S) means for o be OperSymbol of S holds (it . o) = ( QuotArgs (R,o));

      existence

      proof

        defpred P[ object, object] means for o be OperSymbol of S st o = $1 holds $2 = ( QuotArgs (R,o));

        set O = the carrier' of S;

        

         A5: for x be object st x in O holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in O;

          then

          reconsider x1 = x as OperSymbol of S;

          take ( QuotArgs (R,x1));

          thus thesis;

        end;

        consider f be Function such that

         A6: ( dom f) = O & for x be object st x in O holds P[x, (f . x)] from CLASSES1:sch 1( A5);

        reconsider f as ManySortedSet of O by A6, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x1 = x as OperSymbol of S;

          (f . x1) = ( QuotArgs (R,x1)) by A6;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;

        for i be object st i in O holds (f . i) is Function of (((the Sorts of A # ) * the Arity of S) . i), (((( Class R) # ) * the Arity of S) . i)

        proof

          let i be object;

          assume i in O;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotArgs (R,i1)) by A6;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of ((the Sorts of A # ) * the Arity of S), ((( Class R) # ) * the Arity of S) by PBOOLE:def 15;

        take f;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let f,g be ManySortedFunction of ((the Sorts of A # ) * the Arity of S), ((( Class R) # ) * the Arity of S);

        assume that

         A7: for o be OperSymbol of S holds (f . o) = ( QuotArgs (R,o)) and

         A8: for o be OperSymbol of S holds (g . o) = ( QuotArgs (R,o));

        now

          let i be object;

          assume i in the carrier' of S;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotArgs (R,i1)) by A7;

          hence (f . i) = (g . i) by A8;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    theorem :: MSUALG_4:2

    

     Th2: for A be non-empty MSAlgebra over S, R be MSCongruence of A, x be set st x in (((( Class R) # ) * the Arity of S) . o) holds ex a be Element of ( Args (o,A)) st x = (R # a)

    proof

      let A be non-empty MSAlgebra over S, R be MSCongruence of A, x be set;

      assume

       A1: x in (((( Class R) # ) * the Arity of S) . o);

      set ar = ( the_arity_of o);

      

       A2: ar = (the Arity of S . o) by MSUALG_1:def 1;

      then (((( Class R) # ) * the Arity of S) . o) = ( product (( Class R) * ar)) by MSAFREE: 1;

      then

      consider f be Function such that

       A3: f = x and

       A4: ( dom f) = ( dom (( Class R) * ar)) and

       A5: for y be object st y in ( dom (( Class R) * ar)) holds (f . y) in ((( Class R) * ar) . y) by A1, CARD_3:def 5;

      defpred P[ object, object] means $2 in (f . $1);

      

       A6: ( dom (( Class R) * ar)) = ( dom ar) by PARTFUN1:def 2;

      

       A7: for n be Nat st n in ( dom f) holds (f . n) in ( Class (R . (ar /. n)))

      proof

        let n be Nat;

        reconsider s = (ar /. n) as Element of S;

        assume

         A8: n in ( dom f);

        then (ar . n) = (ar /. n) by A4, A6, PARTFUN1:def 6;

        

        then ((( Class R) * ar) . n) = (( Class R) . s) by A4, A8, FUNCT_1: 12

        .= ( Class (R . s)) by Def6;

        hence thesis by A4, A5, A8;

      end;

      

       A9: for a be object st a in ( dom f) holds ex b be object st P[a, b]

      proof

        let a be object;

        reconsider s = (ar /. a) as Element of S;

        assume

         A10: a in ( dom f);

        then

        reconsider n = a as Nat by A4, ORDINAL1:def 12;

        (f . n) in ( Class (R . s)) by A7, A10;

        then

        consider a1 be object such that

         A11: a1 in (the Sorts of A . s) & (f . n) = ( Class ((R . s),a1)) by EQREL_1:def 3;

        take a1;

        thus thesis by A11, EQREL_1: 20;

      end;

      consider g be Function such that

       A12: ( dom g) = ( dom f) & for a be object st a in ( dom f) holds P[a, (g . a)] from CLASSES1:sch 1( A9);

      ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      then ( rng ar) c= ( dom the Sorts of A);

      then

       A13: ( dom g) = ( dom (the Sorts of A * ar)) by A4, A6, A12, RELAT_1: 27;

      

       A14: for y be object st y in ( dom (the Sorts of A * ar)) holds (g . y) in ((the Sorts of A * ar) . y)

      proof

        let y be object;

        assume

         A15: y in ( dom (the Sorts of A * ar));

        then

         A16: (g . y) in (f . y) & (f . y) in ((( Class R) * ar) . y) by A4, A5, A12, A13;

        reconsider n = y as Nat by A15, ORDINAL1:def 12;

        reconsider s = (ar /. n) as Element of S;

        

         A17: (ar . n) = (ar /. n) by A4, A6, A12, A13, A15, PARTFUN1:def 6;

        

        then ((( Class R) * ar) . y) = (( Class R) . s) by A4, A12, A13, A15, FUNCT_1: 12

        .= ( Class (R . s)) by Def6;

        then (g . n) in (the Sorts of A . s) by A16;

        hence thesis by A15, A17, FUNCT_1: 12;

      end;

      ( Args (o,A)) = (((the Sorts of A # ) * the Arity of S) . o) by MSUALG_1:def 4

      .= ( product (the Sorts of A * ar)) by A2, MSAFREE: 1;

      then

      reconsider g as Element of ( Args (o,A)) by A13, A14, CARD_3: 9;

       A18:

      now

        let x be object;

        assume

         A19: x in ( dom ar);

        then

        reconsider n = x as Nat by ORDINAL1:def 12;

        reconsider s = (ar /. n) as Element of S;

        (f . n) in ( Class (R . s)) by A4, A6, A7, A19;

        then

        consider a1 be object such that

         A20: a1 in (the Sorts of A . s) and

         A21: (f . n) = ( Class ((R . s),a1)) by EQREL_1:def 3;

        (g . n) in (f . n) by A4, A6, A12, A19;

        then ( Class ((R . s),(g . n))) = ( Class ((R . s),a1)) by A20, A21, EQREL_1: 23;

        hence (f . x) = ((R # g) . x) by A19, A21, Def7;

      end;

      take g;

      ( dom (R # g)) = ( dom (( Class R) * ar)) by CARD_3: 9;

      hence thesis by A3, A4, A6, A18, FUNCT_1: 2;

    end;

    definition

      let S, o;

      let A be non-empty MSAlgebra over S;

      let R be MSCongruence of A;

      :: MSUALG_4:def12

      func QuotCharact (R,o) -> Function of (((( Class R) # ) * the Arity of S) . o), ((( Class R) * the ResultSort of S) . o) means

      : Def12: for a be Element of ( Args (o,A)) st (R # a) in (((( Class R) # ) * the Arity of S) . o) holds (it . (R # a)) = ((( QuotRes (R,o)) * ( Den (o,A))) . a);

      existence

      proof

        defpred P[ object, object] means for a be Element of ( Args (o,A)) st $1 = (R # a) holds $2 = ((( QuotRes (R,o)) * ( Den (o,A))) . a);

        set Ca = (((( Class R) # ) * the Arity of S) . o), Cr = ((( Class R) * the ResultSort of S) . o);

        

         A1: for x be object st x in Ca holds ex y be object st y in Cr & P[x, y]

        proof

          set ro = ( the_result_sort_of o), ar = ( the_arity_of o);

          let x be object;

          assume x in Ca;

          then

          consider a be Element of ( Args (o,A)) such that

           A2: x = (R # a) by Th2;

          take y = ((( QuotRes (R,o)) * ( Den (o,A))) . a);

          

           A3: o in the carrier' of S;

          then o in ( dom (( Class R) * the ResultSort of S)) by PARTFUN1:def 2;

          

          then

           A4: ((( Class R) * the ResultSort of S) . o) = (( Class R) . (the ResultSort of S . o)) by FUNCT_1: 12

          .= (( Class R) . ro) by MSUALG_1:def 2;

          o in ( dom (the Sorts of A * the ResultSort of S)) by A3, PARTFUN1:def 2;

          

          then

           A5: ((the Sorts of A * the ResultSort of S) . o) = (the Sorts of A . (the ResultSort of S . o)) by FUNCT_1: 12

          .= (the Sorts of A . ro) by MSUALG_1:def 2;

          then

           A6: ( dom ( QuotRes (R,o))) = (the Sorts of A . ro) & ( Result (o,A)) = (the Sorts of A . ro) by FUNCT_2:def 1, MSUALG_1:def 5;

          ( rng ( Den (o,A))) c= ( Result (o,A));

          then

           A7: ( dom ( Den (o,A))) = ( Args (o,A)) & ( dom (( QuotRes (R,o)) * ( Den (o,A)))) = ( dom ( Den (o,A))) by A6, FUNCT_2:def 1, RELAT_1: 27;

          (( QuotRes (R,o)) . (( Den (o,A)) . a)) in ( rng ( QuotRes (R,o))) by A6, FUNCT_1:def 3;

          then (( QuotRes (R,o)) . (( Den (o,A)) . a)) in (( Class R) . ro) by A4;

          hence y in Cr by A4, A7, FUNCT_1: 12;

          let b be Element of ( Args (o,A));

          reconsider da = (( Den (o,A)) . a), db = (( Den (o,A)) . b) as Element of (the Sorts of A . ro) by A5, MSUALG_1:def 5;

          

           A8: ((( QuotRes (R,o)) * ( Den (o,A))) . b) = (( QuotRes (R,o)) . db) by A7, FUNCT_1: 12

          .= ( Class (R,db)) by Def8

          .= ( Class ((R . ro),db));

          assume

           A9: x = (R # b);

          for n be Nat st n in ( dom a) holds [(a . n), (b . n)] in (R . (ar /. n))

          proof

            let n be Nat;

            

             A10: ( dom a) = ( dom ar) by MSUALG_3: 6;

            assume

             A11: n in ( dom a);

            then

             A12: ((R # a) . n) = ( Class ((R . (ar /. n)),(a . n))) & ((R # b) . n) = ( Class ((R . (ar /. n)),(b . n))) by A10, Def7;

            ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

            then ( rng ar) c= ( dom the Sorts of A);

            then

             A13: ( dom (the Sorts of A * ar)) = ( dom ar) by RELAT_1: 27;

            then

             A14: (a . n) in ((the Sorts of A * ar) . n) by A11, A10, MSUALG_3: 6;

            ((the Sorts of A * ar) . n) = (the Sorts of A . (ar . n)) by A13, A11, A10, FUNCT_1: 12

            .= (the Sorts of A . (ar /. n)) by A11, A10, PARTFUN1:def 6;

            hence thesis by A2, A9, A14, A12, EQREL_1: 35;

          end;

          then

           A15: [da, db] in (R . ro) by Def4;

          y = (( QuotRes (R,o)) . (( Den (o,A)) . a)) by A7, FUNCT_1: 12

          .= ( Class (R,da)) by Def8

          .= ( Class ((R . ro),da));

          hence thesis by A8, A15, EQREL_1: 35;

        end;

        consider f be Function such that

         A16: ( dom f) = Ca & ( rng f) c= Cr & for x be object st x in Ca holds P[x, (f . x)] from FUNCT_1:sch 6( A1);

        reconsider f as Function of (((( Class R) # ) * the Arity of S) . o), ((( Class R) * the ResultSort of S) . o) by A16, FUNCT_2: 2;

        take f;

        thus thesis by A16;

      end;

      uniqueness

      proof

        set ao = ( the_arity_of o);

        let F,G be Function of (((( Class R) # ) * the Arity of S) . o), ((( Class R) * the ResultSort of S) . o);

        assume that

         A17: for a be Element of ( Args (o,A)) st (R # a) in (((( Class R) # ) * the Arity of S) . o) holds (F . (R # a)) = ((( QuotRes (R,o)) * ( Den (o,A))) . a) and

         A18: for a be Element of ( Args (o,A)) st (R # a) in (((( Class R) # ) * the Arity of S) . o) holds (G . (R # a)) = ((( QuotRes (R,o)) * ( Den (o,A))) . a);

        

         A19: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

        then ( dom ((( Class R) # ) * the Arity of S)) = ( dom the Arity of S) by PARTFUN1:def 2;

        

        then

         A20: (((( Class R) # ) * the Arity of S) . o) = ((( Class R) # ) . (the Arity of S . o)) by A19, FUNCT_1: 12

        .= ((( Class R) # ) . ao) by MSUALG_1:def 1;

         A21:

        now

          let x be object;

          assume

           A22: x in ((( Class R) # ) . ao);

          then

          consider a be Element of ( Args (o,A)) such that

           A23: x = (R # a) by A20, Th2;

          (F . x) = ((( QuotRes (R,o)) * ( Den (o,A))) . a) by A17, A20, A22, A23;

          hence (F . x) = (G . x) by A18, A20, A22, A23;

        end;

        ( dom F) = ((( Class R) # ) . ao) & ( dom G) = ((( Class R) # ) . ao) by A20, FUNCT_2:def 1;

        hence thesis by A21, FUNCT_1: 2;

      end;

    end

    definition

      let S;

      let A be non-empty MSAlgebra over S;

      let R be MSCongruence of A;

      :: MSUALG_4:def13

      func QuotCharact R -> ManySortedFunction of ((( Class R) # ) * the Arity of S), (( Class R) * the ResultSort of S) means

      : Def13: for o be OperSymbol of S holds (it . o) = ( QuotCharact (R,o));

      existence

      proof

        defpred P[ object, object] means for o be OperSymbol of S st o = $1 holds $2 = ( QuotCharact (R,o));

        set O = the carrier' of S;

        

         A1: for x be object st x in O holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in O;

          then

          reconsider x1 = x as OperSymbol of S;

          take ( QuotCharact (R,x1));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = O & for x be object st x in O holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        reconsider f as ManySortedSet of O by A2, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x1 = x as OperSymbol of S;

          (f . x1) = ( QuotCharact (R,x1)) by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of O by FUNCOP_1:def 6;

        for i be object st i in O holds (f . i) is Function of (((( Class R) # ) * the Arity of S) . i), ((( Class R) * the ResultSort of S) . i)

        proof

          let i be object;

          assume i in O;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotCharact (R,i1)) by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of ((( Class R) # ) * the Arity of S), (( Class R) * the ResultSort of S) by PBOOLE:def 15;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be ManySortedFunction of ((( Class R) # ) * the Arity of S), (( Class R) * the ResultSort of S);

        assume that

         A3: for o be OperSymbol of S holds (f . o) = ( QuotCharact (R,o)) and

         A4: for o be OperSymbol of S holds (g . o) = ( QuotCharact (R,o));

        now

          let i be object;

          assume i in the carrier' of S;

          then

          reconsider i1 = i as OperSymbol of S;

          (f . i1) = ( QuotCharact (R,i1)) by A3;

          hence (f . i) = (g . i) by A4;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    definition

      let S;

      let U1 be non-empty MSAlgebra over S;

      let R be MSCongruence of U1;

      :: MSUALG_4:def14

      func QuotMSAlg (U1,R) -> MSAlgebra over S equals MSAlgebra (# ( Class R), ( QuotCharact R) #);

      coherence ;

    end

    registration

      let S;

      let U1 be non-empty MSAlgebra over S;

      let R be MSCongruence of U1;

      cluster ( QuotMSAlg (U1,R)) -> strict non-empty;

      coherence by MSUALG_1:def 3;

    end

    definition

      let S;

      let U1 be non-empty MSAlgebra over S;

      let R be MSCongruence of U1;

      let s be SortSymbol of S;

      :: MSUALG_4:def15

      func MSNat_Hom (U1,R,s) -> Function of (the Sorts of U1 . s), (( Class R) . s) means

      : Def15: for x be set st x in (the Sorts of U1 . s) holds (it . x) = ( Class ((R . s),x));

      existence

      proof

        deffunc F( object) = ( Class ((R . s),$1));

        consider f be Function such that

         A1: ( dom f) = (the Sorts of U1 . s) & for x be object st x in (the Sorts of U1 . s) holds (f . x) = F(x) from FUNCT_1:sch 3;

        for x be object st x in (the Sorts of U1 . s) holds (f . x) in (( Class R) . s)

        proof

          let x be object;

          assume

           A2: x in (the Sorts of U1 . s);

          then ( Class ((R . s),x)) in ( Class (R . s)) by EQREL_1:def 3;

          then (f . x) in ( Class (R . s)) by A1, A2;

          hence thesis by Def6;

        end;

        then

        reconsider f as Function of (the Sorts of U1 . s), (( Class R) . s) by A1, FUNCT_2: 3;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function of (the Sorts of U1 . s), (( Class R) . s);

        assume that

         A3: for x be set st x in (the Sorts of U1 . s) holds (f . x) = ( Class ((R . s),x)) and

         A4: for x be set st x in (the Sorts of U1 . s) holds (g . x) = ( Class ((R . s),x));

         A5:

        now

          let x be object;

          assume

           A6: x in (the Sorts of U1 . s);

          then (f . x) = ( Class ((R . s),x)) by A3;

          hence (f . x) = (g . x) by A4, A6;

        end;

        ( dom f) = (the Sorts of U1 . s) & ( dom g) = (the Sorts of U1 . s) by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1: 2;

      end;

    end

    definition

      let S;

      let U1 be non-empty MSAlgebra over S;

      let R be MSCongruence of U1;

      :: MSUALG_4:def16

      func MSNat_Hom (U1,R) -> ManySortedFunction of U1, ( QuotMSAlg (U1,R)) means

      : Def16: for s be SortSymbol of S holds (it . s) = ( MSNat_Hom (U1,R,s));

      existence

      proof

        deffunc F( Element of S) = ( MSNat_Hom (U1,R,$1));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = F(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider y = x as Element of S;

          (f . y) = ( MSNat_Hom (U1,R,y)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;

        for i be object st i in the carrier of S holds (f . i) is Function of (the Sorts of U1 . i), (( Class R) . i)

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          (f . s) = ( MSNat_Hom (U1,R,s)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of the Sorts of U1, ( Class R) by PBOOLE:def 15;

        reconsider f as ManySortedFunction of U1, ( QuotMSAlg (U1,R));

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be ManySortedFunction of U1, ( QuotMSAlg (U1,R));

        assume that

         A2: for s be SortSymbol of S holds (F . s) = ( MSNat_Hom (U1,R,s)) and

         A3: for s be SortSymbol of S holds (G . s) = ( MSNat_Hom (U1,R,s));

        now

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as SortSymbol of S;

          (F . s) = ( MSNat_Hom (U1,R,s)) by A2;

          hence (F . i) = (G . i) by A3;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    theorem :: MSUALG_4:3

    for U1 be non-empty MSAlgebra over S, R be MSCongruence of U1 holds ( MSNat_Hom (U1,R)) is_epimorphism (U1,( QuotMSAlg (U1,R)))

    proof

      let U1 be non-empty MSAlgebra over S, R be MSCongruence of U1;

      set F = ( MSNat_Hom (U1,R)), QA = ( QuotMSAlg (U1,R)), S1 = the Sorts of U1;

      for o be OperSymbol of S st ( Args (o,U1)) <> {} holds for x be Element of ( Args (o,U1)) holds ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,QA)) . (F # x))

      proof

        let o be OperSymbol of S such that ( Args (o,U1)) <> {} ;

        let x be Element of ( Args (o,U1));

        set ro = ( the_result_sort_of o), ar = ( the_arity_of o);

        (the Arity of S . o) = ar by MSUALG_1:def 1;

        then

         A1: (((( Class R) # ) * the Arity of S) . o) = ( product (( Class R) * ar)) by MSAFREE: 1;

        

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

        

         A3: for a be object st a in ( dom ar) holds ((F # x) . a) = ((R # x) . a)

        proof

          let a be object;

          assume

           A4: a in ( dom ar);

          then

          reconsider n = a as Nat by ORDINAL1:def 12;

          set Fo = ( MSNat_Hom (U1,R,(ar /. n))), s = (ar /. n);

          

           A5: n in ( dom (the Sorts of U1 * ar)) by A4, PARTFUN1:def 2;

          

          then ((the Sorts of U1 * ar) . n) = (the Sorts of U1 . (ar . n)) by FUNCT_1: 12

          .= (S1 . s) by A4, PARTFUN1:def 6;

          then

          reconsider xn = (x . n) as Element of (S1 . s) by A5, MSUALG_3: 6;

          

          thus ((F # x) . a) = ((F . (ar /. n)) . (x . n)) by A2, A4, MSUALG_3:def 6

          .= (Fo . xn) by Def16

          .= ( Class ((R . s),(x . n))) by Def15

          .= ((R # x) . a) by A4, Def7;

        end;

        ( dom the Sorts of U1) = the carrier of S by PARTFUN1:def 2;

        then ( rng the ResultSort of S) c= ( dom the Sorts of U1);

        then ( dom the ResultSort of S) = the carrier' of S & ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by FUNCT_2:def 1, RELAT_1: 27;

        

        then

         A6: ((the Sorts of U1 * the ResultSort of S) . o) = (the Sorts of U1 . (the ResultSort of S . o)) by FUNCT_1: 12

        .= (the Sorts of U1 . ro) by MSUALG_1:def 2;

        then

        reconsider dx = (( Den (o,U1)) . x) as Element of (S1 . ro) by MSUALG_1:def 5;

        ( rng ( Den (o,U1))) c= ( Result (o,U1)) & ( Result (o,U1)) = (S1 . ro) by A6, MSUALG_1:def 5;

        then ( rng ( Den (o,U1))) c= ( dom ( QuotRes (R,o))) by A6, FUNCT_2:def 1;

        then

         A7: ( dom ( Den (o,U1))) = ( Args (o,U1)) & ( dom (( QuotRes (R,o)) * ( Den (o,U1)))) = ( dom ( Den (o,U1))) by FUNCT_2:def 1, RELAT_1: 27;

        ( dom ( Class R)) = the carrier of S by PARTFUN1:def 2;

        then ( dom (R # x)) = ( dom (( Class R) * ( the_arity_of o))) & ( rng ar) c= ( dom ( Class R)) by CARD_3: 9;

        then ( dom (F # x)) = ( dom ar) & ( dom (R # x)) = ( dom ar) by MSUALG_3: 6, RELAT_1: 27;

        then

         A8: (F # x) = (R # x) by A3, FUNCT_1: 2;

        ( Den (o,QA)) = (( QuotCharact R) . o) by MSUALG_1:def 6

        .= ( QuotCharact (R,o)) by Def13;

        

        then (( Den (o,QA)) . (F # x)) = ((( QuotRes (R,o)) * ( Den (o,U1))) . x) by A1, A8, Def12

        .= (( QuotRes (R,o)) . dx) by A7, FUNCT_1: 12

        .= ( Class (R,dx)) by Def8

        .= (( MSNat_Hom (U1,R,ro)) . dx) by Def15

        .= ((F . ro) . (( Den (o,U1)) . x)) by Def16;

        hence thesis;

      end;

      hence F is_homomorphism (U1,QA);

      for i be set st i in the carrier of S holds ( rng (F . i)) = (the Sorts of QA . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then

        reconsider s = i as Element of S;

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

        

         A9: ( dom f) = (S1 . s) by FUNCT_2:def 1;

        

         A10: (the Sorts of QA . s) = ( Class (R . s)) by Def6;

        for x be object st x in (the Sorts of QA . i) holds x in ( rng f)

        proof

          let x be object;

          

           A11: f = ( MSNat_Hom (U1,R,s)) by Def16;

          assume x in (the Sorts of QA . i);

          then

          consider a1 be object such that

           A12: a1 in (S1 . s) and

           A13: x = ( Class ((R . s),a1)) by A10, EQREL_1:def 3;

          (f . a1) in ( rng f) by A9, A12, FUNCT_1:def 3;

          hence thesis by A12, A13, A11, Def15;

        end;

        then (the Sorts of QA . i) c= ( rng f);

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      let s be SortSymbol of S;

      :: MSUALG_4:def17

      func MSCng (F,s) -> Equivalence_Relation of (the Sorts of U1 . s) means

      : Def17: for x,y be Element of (the Sorts of U1 . s) holds [x, y] in it iff ((F . s) . x) = ((F . s) . y);

      existence

      proof

        defpred P[ object, object] means ((F . s) . $1) = ((F . s) . $2);

        set S1 = (the Sorts of U1 . s);

        

         A1: for x,y be object st P[x, y] holds P[y, x];

        

         A2: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z];

        

         A3: for x be object st x in S1 holds P[x, x];

        consider R be Equivalence_Relation of S1 such that

         A4: for x,y be object holds [x, y] in R iff x in S1 & y in S1 & P[x, y] from EQREL_1:sch 1( A3, A1, A2);

        take R;

        let x,y be Element of (the Sorts of U1 . s);

        thus thesis by A4;

      end;

      uniqueness

      proof

        let R,S be Equivalence_Relation of (the Sorts of U1 . s);

        assume that

         A5: for x,y be Element of (the Sorts of U1 . s) holds [x, y] in R iff ((F . s) . x) = ((F . s) . y) and

         A6: for x,y be Element of (the Sorts of U1 . s) holds [x, y] in S iff ((F . s) . x) = ((F . s) . y);

        now

          let x,y be object;

          thus [x, y] in R implies [x, y] in S

          proof

            assume

             A7: [x, y] in R;

            then

            reconsider a = x, b = y as Element of (the Sorts of U1 . s) by ZFMISC_1: 87;

            ((F . s) . a) = ((F . s) . b) by A5, A7;

            hence thesis by A6;

          end;

          assume

           A8: [x, y] in S;

          then

          reconsider a = x, b = y as Element of (the Sorts of U1 . s) by ZFMISC_1: 87;

          ((F . s) . a) = ((F . s) . b) by A6, A8;

          hence [x, y] in R by A5;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      assume

       A1: F is_homomorphism (U1,U2);

      :: MSUALG_4:def18

      func MSCng (F) -> MSCongruence of U1 means

      : Def18: for s be SortSymbol of S holds (it . s) = ( MSCng (F,s));

      existence

      proof

        deffunc F( Element of S) = ( MSCng (F,$1));

        consider f be Function such that

         A2: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = F(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A2, PARTFUN1:def 2, RELAT_1:def 18;

        for i be set st i in the carrier of S holds (f . i) is Relation of (the Sorts of U1 . i), (the Sorts of U1 . i)

        proof

          let i be set;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          (f . i) = ( MSCng (F,s)) by A2;

          hence thesis;

        end;

        then

        reconsider f as ManySortedRelation of the Sorts of U1 by Def1;

        reconsider f as ManySortedRelation of U1;

        for i be set, R be Relation of (the Sorts of U1 . i) st i in the carrier of S & (f . i) = R holds R is Equivalence_Relation of (the Sorts of U1 . i)

        proof

          let i be set, R be Relation of (the Sorts of U1 . i);

          assume that

           A3: i in the carrier of S and

           A4: (f . i) = R;

          reconsider s = i as Element of S by A3;

          R = ( MSCng (F,s)) by A2, A4;

          hence thesis;

        end;

        then f is MSEquivalence_Relation-like;

        then

        reconsider f as MSEquivalence-like ManySortedRelation of U1 by Def3;

        for o be OperSymbol of S, x,y be Element of ( Args (o,U1)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (f . (( the_arity_of o) /. n))) holds [(( Den (o,U1)) . x), (( Den (o,U1)) . y)] in (f . ( the_result_sort_of o))

        proof

          let o be OperSymbol of S, x,y be Element of ( Args (o,U1));

          set ao = ( the_arity_of o), ro = ( the_result_sort_of o), S1 = the Sorts of U1;

          

           A5: ( dom x) = ( dom ( the_arity_of o)) by MSUALG_3: 6;

          

           A6: ( dom y) = ( dom ( the_arity_of o)) by MSUALG_3: 6;

          assume

           A7: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (f . (( the_arity_of o) /. n));

           A8:

          now

            let n be object;

            assume

             A9: n in ( dom ( the_arity_of o));

            then

            reconsider m = n as Nat by ORDINAL1:def 12;

            

             A10: ((F # x) . m) = ((F . (ao /. m)) . (x . m)) & ((F # y) . m) = ((F . (ao /. m)) . (y . m)) by A5, A6, A9, MSUALG_3:def 6;

            (ao . m) in ( rng ao) by A9, FUNCT_1:def 3;

            then

            reconsider s = (ao . m) as SortSymbol of S;

            

             A11: n in ( dom (S1 * ao)) by A9, PARTFUN1:def 2;

            then (x . m) in ((S1 * ao) . n) & (y . m) in ((S1 * ao) . n) by MSUALG_3: 6;

            then

            reconsider x1 = (x . m), y1 = (y . m) as Element of (S1 . s) by A11, FUNCT_1: 12;

            

             A12: [x1, y1] in (f . (ao /. m)) by A7, A5, A9;

            

             A13: (ao /. m) = (ao . m) by A9, PARTFUN1:def 6;

            then (f . (ao /. m)) = ( MSCng (F,s)) by A2;

            hence ((F # x) . n) = ((F # y) . n) by A10, A13, A12, Def17;

          end;

          ( dom (F # x)) = ( dom ( the_arity_of o)) & ( dom (F # y)) = ( dom ( the_arity_of o)) by MSUALG_3: 6;

          then

           A14: (F # x) = (F # y) by A8, FUNCT_1: 2;

          reconsider ro as SortSymbol of S;

          

           A15: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

          then

           A16: ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by PARTFUN1:def 2;

          ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) by MSUALG_1:def 5

          .= (the Sorts of U1 . (the ResultSort of S . o)) by A15, A16, FUNCT_1: 12

          .= (the Sorts of U1 . ro) by MSUALG_1:def 2;

          then

          reconsider Dx = (( Den (o,U1)) . x), Dy = (( Den (o,U1)) . y) as Element of (the Sorts of U1 . ro);

          

           A17: ((F . ro) . Dy) = (( Den (o,U2)) . (F # y)) by A1;

          (f . ro) = ( MSCng (F,ro)) & ((F . ro) . Dx) = (( Den (o,U2)) . (F # x)) by A1, A2;

          hence thesis by A14, A17, Def17;

        end;

        then

        reconsider f as MSCongruence of U1 by Def4;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let C1,C2 be MSCongruence of U1;

        assume that

         A18: for s be SortSymbol of S holds (C1 . s) = ( MSCng (F,s)) and

         A19: for s be SortSymbol of S holds (C2 . s) = ( MSCng (F,s));

        now

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          (C1 . s) = ( MSCng (F,s)) by A18;

          hence (C1 . i) = (C2 . i) by A19;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      let s be SortSymbol of S;

      assume

       A1: F is_homomorphism (U1,U2);

      :: MSUALG_4:def19

      func MSHomQuot (F,s) -> Function of (the Sorts of ( QuotMSAlg (U1,( MSCng F))) . s), (the Sorts of U2 . s) means

      : Def19: for x be Element of (the Sorts of U1 . s) holds (it . ( Class (( MSCng (F,s)),x))) = ((F . s) . x);

      existence

      proof

        set qa = ( QuotMSAlg (U1,( MSCng F))), cqa = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2;

        defpred P[ object, object] means for a be Element of (S1 . s) st $1 = ( Class (( MSCng (F,s)),a)) holds $2 = ((F . s) . a);

        

         A2: (cqa . s) = ( Class (( MSCng F) . s)) by Def6

        .= ( Class ( MSCng (F,s))) by A1, Def18;

        

         A3: for x be object st x in (cqa . s) holds ex y be object st y in (S2 . s) & P[x, y]

        proof

          let x be object;

          assume

           A4: x in (cqa . s);

          then

          reconsider x1 = x as Subset of (S1 . s) by A2;

          consider a be object such that

           A5: a in (S1 . s) and

           A6: x1 = ( Class (( MSCng (F,s)),a)) by A2, A4, EQREL_1:def 3;

          reconsider a as Element of (S1 . s) by A5;

          take y = ((F . s) . a);

          thus y in (S2 . s);

          let b be Element of (S1 . s);

          assume x = ( Class (( MSCng (F,s)),b));

          then b in ( Class (( MSCng (F,s)),a)) by A6, EQREL_1: 23;

          then [b, a] in ( MSCng (F,s)) by EQREL_1: 19;

          hence thesis by Def17;

        end;

        consider G be Function such that

         A7: ( dom G) = (cqa . s) & ( rng G) c= (S2 . s) & for x be object st x in (cqa . s) holds P[x, (G . x)] from FUNCT_1:sch 6( A3);

        reconsider G as Function of (cqa . s), (S2 . s) by A7, FUNCT_2:def 1, RELSET_1: 4;

        take G;

        let a be Element of (S1 . s);

        ( Class (( MSCng (F,s)),a)) in ( Class ( MSCng (F,s))) by EQREL_1:def 3;

        hence thesis by A2, A7;

      end;

      uniqueness

      proof

        set qa = ( QuotMSAlg (U1,( MSCng F))), cqa = the Sorts of qa, u1 = the Sorts of U1, u2 = the Sorts of U2;

        let H,G be Function of (cqa . s), (u2 . s);

        assume that

         A8: for a be Element of (u1 . s) holds (H . ( Class (( MSCng (F,s)),a))) = ((F . s) . a) and

         A9: for a be Element of (u1 . s) holds (G . ( Class (( MSCng (F,s)),a))) = ((F . s) . a);

        

         A10: (cqa . s) = ( Class (( MSCng F) . s)) by Def6

        .= ( Class ( MSCng (F,s))) by A1, Def18;

        for x be object st x in (cqa . s) holds (H . x) = (G . x)

        proof

          let x be object;

          assume

           A11: x in (cqa . s);

          then

          reconsider x1 = x as Subset of (u1 . s) by A10;

          consider a be object such that

           A12: a in (u1 . s) and

           A13: x1 = ( Class (( MSCng (F,s)),a)) by A10, A11, EQREL_1:def 3;

          reconsider a as Element of (u1 . s) by A12;

          

          thus (H . x) = ((F . s) . a) by A8, A13

          .= (G . x) by A9, A13;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      :: MSUALG_4:def20

      func MSHomQuot (F) -> ManySortedFunction of ( QuotMSAlg (U1,( MSCng F))), U2 means

      : Def20: for s be SortSymbol of S holds (it . s) = ( MSHomQuot (F,s));

      existence

      proof

        deffunc G( Element of S) = ( MSHomQuot (F,$1));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for d be Element of S holds (f . d) = G(d) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider y = x as Element of S;

          (f . y) = ( MSHomQuot (F,y)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;

        for i be object st i in the carrier of S holds (f . i) is Function of (the Sorts of ( QuotMSAlg (U1,( MSCng F))) . i), (the Sorts of U2 . i)

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as Element of S;

          (f . s) = ( MSHomQuot (F,s)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of the Sorts of ( QuotMSAlg (U1,( MSCng F))), the Sorts of U2 by PBOOLE:def 15;

        reconsider f as ManySortedFunction of ( QuotMSAlg (U1,( MSCng F))), U2;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let H,G be ManySortedFunction of ( QuotMSAlg (U1,( MSCng F))), U2;

        assume that

         A2: for s be SortSymbol of S holds (H . s) = ( MSHomQuot (F,s)) and

         A3: for s be SortSymbol of S holds (G . s) = ( MSHomQuot (F,s));

        now

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as SortSymbol of S;

          (H . s) = ( MSHomQuot (F,s)) by A2;

          hence (H . i) = (G . i) by A3;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    theorem :: MSUALG_4:4

    

     Th4: for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) holds ( MSHomQuot F) is_monomorphism (( QuotMSAlg (U1,( MSCng F))),U2)

    proof

      let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2;

      set mc = ( MSCng F), qa = ( QuotMSAlg (U1,mc)), qh = ( MSHomQuot F), S1 = the Sorts of U1;

      assume

       A1: F is_homomorphism (U1,U2);

      for o be OperSymbol of S st ( Args (o,qa)) <> {} holds for x be Element of ( Args (o,qa)) holds ((qh . ( the_result_sort_of o)) . (( Den (o,qa)) . x)) = (( Den (o,U2)) . (qh # x))

      proof

        let o be OperSymbol of S such that ( Args (o,qa)) <> {} ;

        let x be Element of ( Args (o,qa));

        set ro = ( the_result_sort_of o), ar = ( the_arity_of o);

        

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

        ( Args (o,qa)) = (((( Class mc) # ) * the Arity of S) . o) by MSUALG_1:def 4;

        then

        consider a be Element of ( Args (o,U1)) such that

         A3: x = (mc # a) by Th2;

        

         A4: ( dom a) = ( dom ar) by MSUALG_3: 6;

         A5:

        now

          let y be object;

          assume

           A6: y in ( dom ar);

          then

          reconsider n = y as Nat by ORDINAL1:def 12;

          (ar . n) in ( rng ar) by A6, FUNCT_1:def 3;

          then

          reconsider s = (ar . n) as SortSymbol of S;

          

           A7: (ar /. n) = (ar . n) by A6, PARTFUN1:def 6;

          then (x . n) = ( Class ((mc . s),(a . n))) by A3, A6, Def7;

          then

           A8: (x . n) = ( Class (( MSCng (F,s)),(a . n))) by A1, Def18;

          

           A9: n in ( dom (S1 * ar)) by A6, PARTFUN1:def 2;

          then (a . n) in ((S1 * ar) . n) by MSUALG_3: 6;

          then

          reconsider an = (a . n) as Element of (S1 . s) by A9, FUNCT_1: 12;

          ((qh # x) . n) = ((qh . s) . (x . n)) by A2, A6, A7, MSUALG_3:def 6

          .= (( MSHomQuot (F,s)) . (x . n)) by Def20

          .= ((F . s) . an) by A1, A8, Def19

          .= ((F # a) . n) by A4, A6, A7, MSUALG_3:def 6;

          hence ((qh # x) . y) = ((F # a) . y);

        end;

        o in the carrier' of S;

        then o in ( dom (S1 * the ResultSort of S)) by PARTFUN1:def 2;

        

        then

         A10: ((the Sorts of U1 * the ResultSort of S) . o) = (the Sorts of U1 . (the ResultSort of S . o)) by FUNCT_1: 12

        .= (the Sorts of U1 . ro) by MSUALG_1:def 2;

        then ( rng ( Den (o,U1))) c= ( Result (o,U1)) & ( Result (o,U1)) = (S1 . ro) by MSUALG_1:def 5;

        then ( rng ( Den (o,U1))) c= ( dom ( QuotRes (mc,o))) by A10, FUNCT_2:def 1;

        then

         A11: ( dom ( Den (o,U1))) = ( Args (o,U1)) & ( dom (( QuotRes (mc,o)) * ( Den (o,U1)))) = ( dom ( Den (o,U1))) by FUNCT_2:def 1, RELAT_1: 27;

        ar = (the Arity of S . o) by MSUALG_1:def 1;

        then

         A12: ( product (( Class mc) * ar)) = (((( Class mc) # ) * the Arity of S) . o) by MSAFREE: 1;

        reconsider da = (( Den (o,U1)) . a) as Element of (S1 . ro) by A10, MSUALG_1:def 5;

        

         A13: (qh . ro) = ( MSHomQuot (F,ro)) by Def20;

        ( Den (o,qa)) = (( QuotCharact mc) . o) by MSUALG_1:def 6

        .= ( QuotCharact (mc,o)) by Def13;

        

        then (( Den (o,qa)) . x) = ((( QuotRes (mc,o)) * ( Den (o,U1))) . a) by A3, A12, Def12

        .= (( QuotRes (mc,o)) . da) by A11, FUNCT_1: 12

        .= ( Class (mc,da)) by Def8

        .= ( Class (( MSCng (F,ro)),da)) by A1, Def18;

        

        then

         A14: ((qh . ro) . (( Den (o,qa)) . x)) = ((F . ro) . (( Den (o,U1)) . a)) by A1, A13, Def19

        .= (( Den (o,U2)) . (F # a)) by A1;

        ( dom (qh # x)) = ( dom ar) & ( dom (F # a)) = ( dom ar) by MSUALG_3: 6;

        hence thesis by A5, A14, FUNCT_1: 2;

      end;

      hence qh is_homomorphism (qa,U2);

      for i be set st i in the carrier of S holds (qh . i) is one-to-one

      proof

        let i be set;

        set f = (qh . i);

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A15: f = ( MSHomQuot (F,s)) by Def20;

        for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume that

           A16: x1 in ( dom f) and

           A17: x2 in ( dom f) and

           A18: (f . x1) = (f . x2);

          x1 in (( Class mc) . s) by A15, A16, FUNCT_2:def 1;

          then x1 in ( Class (mc . s)) by Def6;

          then

          consider a1 be object such that

           A19: a1 in (S1 . s) and

           A20: x1 = ( Class ((mc . s),a1)) by EQREL_1:def 3;

          x2 in (( Class mc) . s) by A15, A17, FUNCT_2:def 1;

          then x2 in ( Class (mc . s)) by Def6;

          then

          consider a2 be object such that

           A21: a2 in (S1 . s) and

           A22: x2 = ( Class ((mc . s),a2)) by EQREL_1:def 3;

          reconsider a2 as Element of (S1 . s) by A21;

          

           A23: (mc . s) = ( MSCng (F,s)) by A1, Def18;

          then

           A24: (f . x2) = ((F . s) . a2) by A1, A15, A22, Def19;

          reconsider a1 as Element of (S1 . s) by A19;

          (f . x1) = ((F . s) . a1) by A1, A15, A23, A20, Def19;

          then [a1, a2] in ( MSCng (F,s)) by A18, A24, Def17;

          hence thesis by A23, A20, A22, EQREL_1: 35;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

      hence thesis by MSUALG_3: 1;

    end;

    theorem :: MSUALG_4:5

    

     Th5: for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2 st F is_epimorphism (U1,U2) holds ( MSHomQuot F) is_isomorphism (( QuotMSAlg (U1,( MSCng F))),U2)

    proof

      let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2;

      set mc = ( MSCng F), qa = ( QuotMSAlg (U1,mc)), qh = ( MSHomQuot F);

      set Sq = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2;

      assume

       A1: F is_epimorphism (U1,U2);

      then

       A2: F is_homomorphism (U1,U2);

      

       A3: F is "onto" by A1;

      for i be set st i in the carrier of S holds ( rng (qh . i)) = (S2 . i)

      proof

        let i be set;

        set f = (qh . i);

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A4: ( rng (F . s)) = (S2 . s) by A3;

        

         A5: (qh . i) = ( MSHomQuot (F,s)) by Def20;

        hence ( rng f) c= (S2 . i) by RELAT_1:def 19;

        let x be object;

        assume x in (S2 . i);

        then

        consider a be object such that

         A6: a in ( dom (F . s)) and

         A7: ((F . s) . a) = x by A4, FUNCT_1:def 3;

        

         A8: ( MSCng (F,s)) = (( MSCng F) . s) & (Sq . s) = ( Class (( MSCng F) . s)) by A2, Def6, Def18;

        reconsider a as Element of (S1 . s) by A6;

        ( dom f) = (Sq . s) by A5, FUNCT_2:def 1;

        then

         A9: ( Class (( MSCng (F,s)),a)) in ( dom f) by A8, EQREL_1:def 3;

        (f . ( Class (( MSCng (F,s)),a))) = x by A2, A5, A7, Def19;

        hence thesis by A9, FUNCT_1:def 3;

      end;

      then

       A10: qh is "onto";

      qh is_monomorphism (qa,U2) by A2, Th4;

      then qh is_homomorphism (qa,U2) & qh is "1-1";

      hence thesis by A10, MSUALG_3: 13;

    end;

    theorem :: MSUALG_4:6

    for U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2 st F is_epimorphism (U1,U2) holds (( QuotMSAlg (U1,( MSCng F))),U2) are_isomorphic

    proof

      let U1,U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2;

      assume F is_epimorphism (U1,U2);

      then ( MSHomQuot F) is_isomorphism (( QuotMSAlg (U1,( MSCng F))),U2) by Th5;

      hence thesis;

    end;