:: Many Sorted Quotient Algebra
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received May 6, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users


registration
let I be set ;
cluster Relation-like I -defined Function-like total Relation-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is Relation-yielding
proof end;
end;

definition
let I be set ;
let A, B be ManySortedSet of I;
mode ManySortedRelation of A,B -> ManySortedSet of I means :Def1: :: MSUALG_4:def 1
 for i being set st i in I holds
it . i is Relation of (A . i),(B . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Relation of (A . i),(B . i)
proof end;
end;

:: deftheorem Def1 defines ManySortedRelation MSUALG_4:def 1 :
for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedRelation of A,B iff for i being set st i in I holds
b4 . i is Relation of (A . i),(B . i) );

registration
let I be set ;
let A, B be ManySortedSet of I;
cluster -> Relation-yielding for ManySortedRelation of A,B;
coherence
for b1 being ManySortedRelation of A,B holds b1 is Relation-yielding
proof end;
end;

definition
let I be set ;
let A be ManySortedSet of I;
mode ManySortedRelation of A is ManySortedRelation of A,A;
end;

definition
let I be set ;
let A be ManySortedSet of I;
let IT be ManySortedRelation of A;
attr IT is MSEquivalence_Relation-like means :Def2: :: MSUALG_4:def 2
 for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i);
end;

:: deftheorem Def2 defines MSEquivalence_Relation-like MSUALG_4:def 2 :
for I being set
for A being ManySortedSet of I
for IT being ManySortedRelation of A holds
( IT is MSEquivalence_Relation-like iff for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i) );

definition
let I be non empty set ;
let A, B be ManySortedSet of I;
let F be ManySortedRelation of A,B;
let i be Element of I;
:: original: .
redefine func F . i -> Relation of (A . i),(B . i);
coherence
F . i is Relation of (A . i),(B . i) by Def1;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
let IT be ManySortedRelation of U1;
attr IT is MSEquivalence-like means :Def3: :: MSUALG_4:def 3
IT is MSEquivalence_Relation-like ;
end;

:: deftheorem Def3 defines MSEquivalence-like MSUALG_4:def 3 :
for S being non empty ManySortedSign
for U1 being MSAlgebra over S
for IT being ManySortedRelation of U1 holds
( IT is MSEquivalence-like iff IT is MSEquivalence_Relation-like );

registration
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1;
existence
ex b1 being ManySortedRelation of U1 st b1 is MSEquivalence-like
proof end;
end;

theorem Th1: :: MSUALG_4:1
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for s being SortSymbol of S
for R being 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 empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
attr R is MSCongruence-like means :Def4: :: MSUALG_4:def 4
 for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being 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;

:: deftheorem Def4 defines MSCongruence-like MSUALG_4:def 4 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1 holds
( R is MSCongruence-like iff for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being 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) );

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1;
existence
ex b1 being MSEquivalence-like ManySortedRelation of U1 st b1 is MSCongruence-like
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
mode MSCongruence of U1 is MSEquivalence-like MSCongruence-like ManySortedRelation of U1;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
let i be Element of S;
:: original: .
redefine func R . i -> Equivalence_Relation of ( the Sorts of U1 . i);
coherence
R . i is Equivalence_Relation of ( the Sorts of U1 . i) by Th1;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
let i be Element of S;
let x be Element of the Sorts of U1 . i;
func Class (R,x) -> Subset of ( the Sorts of U1 . i) equals :: MSUALG_4:def 5
 Class ((R . i),x);
correctness
coherence
Class ((R . i),x) is Subset of ( the Sorts of U1 . i);
;
end;

:: deftheorem defines Class MSUALG_4:def 5 :
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1
for i being Element of S
for x being Element of the Sorts of U1 . i holds Class (R,x) = Class ((R . i),x);

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func Class R -> V8() ManySortedSet of the carrier of S means :Def6: :: MSUALG_4:def 6
 for s being Element of S holds it . s = Class (R . s);
existence
ex b1 being V8() ManySortedSet of the carrier of S st
for s being Element of S holds b1 . s = Class (R . s)
proof end;
uniqueness
for b1, b2 being V8() ManySortedSet of the carrier of S st ( for s being Element of S holds b1 . s = Class (R . s) ) & ( for s being Element of S holds b2 . s = Class (R . s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Class MSUALG_4:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b4 being V8() ManySortedSet of the carrier of S holds
( b4 = Class R iff for s being Element of S holds b4 . s = Class (R . s) );

definition
let S be non empty non void ManySortedSign ;
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
F . o is Function of (M1 . o),(M2 . o) by PBOOLE:def 15;
end;

registration
let I be non empty set ;
let p be FinSequence of I;
let X be ManySortedSet of I;
cluster p * X -> dom p -defined for Function;
coherence
for b1 being Function st b1 = X * p holds
b1 is dom p -defined
proof end;
end;

registration
let I be non empty set ;
let p be FinSequence of I;
let X be ManySortedSet of I;
cluster p * X -> dom p -defined total for dom p -defined Function;
coherence
for b1 being dom p -defined Function st b1 = X * p holds
b1 is total
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
let x be Element of Args (o,A);
func R # x -> Element of product ((Class R) * (the_arity_of o)) means :Def7: :: MSUALG_4:def 7
 for n being Nat st n in dom (the_arity_of o) holds
it . n = Class ((R . ((the_arity_of o) /. n)),(x . n));
existence
ex b1 being Element of product ((Class R) * (the_arity_of o)) st
for n being Nat st n in dom (the_arity_of o) holds
b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n))
proof end;
uniqueness
for b1, b2 being Element of product ((Class R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds
b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds
b2 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines # MSUALG_4:def 7 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being Element of Args (o,A)
for b6 being Element of product ((Class R) * (the_arity_of o)) holds
( b6 = R # x iff for n being Nat st n in dom (the_arity_of o) holds
b6 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) );

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes (R,o) -> Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) means :Def8: :: MSUALG_4:def 8
 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = Class (R,x);
existence
ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st
for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x)
proof end;
uniqueness
for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = Class (R,x) ) holds
b1 = b2
proof end;
func QuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) means :: MSUALG_4:def 9
 for x being Element of Args (o,A) holds it . x = R # x;
existence
ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st
for x being Element of Args (o,A) holds b1 . x = R # x
proof end;
uniqueness
for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R # x ) & ( for x being Element of Args (o,A) holds b2 . x = R # x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines QuotRes MSUALG_4:def 8 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = Class (R,x) );

:: deftheorem defines QuotArgs MSUALG_4:def 9 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) holds
( b5 = QuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R # x );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes R -> ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S means :: MSUALG_4:def 10
 for o being OperSymbol of S holds it . o = QuotRes (R,o);
existence
ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = QuotRes (R,o)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotRes (R,o) ) holds
b1 = b2
proof end;
func QuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S means :: MSUALG_4:def 11
 for o being OperSymbol of S holds it . o = QuotArgs (R,o);
existence
ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st
for o being OperSymbol of S holds b1 . o = QuotArgs (R,o)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotArgs (R,o) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines QuotRes MSUALG_4:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S holds
( b4 = QuotRes R iff for o being OperSymbol of S holds b4 . o = QuotRes (R,o) );

:: deftheorem defines QuotArgs MSUALG_4:def 11 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds
( b4 = QuotArgs R iff for o being OperSymbol of S holds b4 . o = QuotArgs (R,o) );

theorem Th2: :: MSUALG_4:2
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
proof end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact (R,o) -> Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) means :Def12: :: MSUALG_4:def 12
 for a being 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
ex b1 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st
for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a
proof end;
uniqueness
for b1, b2 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b2 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines QuotCharact MSUALG_4:def 12 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b5 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact R -> ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S means :Def13: :: MSUALG_4:def 13
 for o being OperSymbol of S holds it . o = QuotCharact (R,o);
existence
ex b1 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = QuotCharact (R,o)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotCharact (R,o) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines QuotCharact MSUALG_4:def 13 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds
( b4 = QuotCharact R iff for o being OperSymbol of S holds b4 . o = QuotCharact (R,o) );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func QuotMSAlg (U1,R) -> MSAlgebra over S equals :: MSUALG_4:def 14
 MSAlgebra(# (Class R),(QuotCharact R) #);
coherence
MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra over S ;
end;

:: deftheorem defines QuotMSAlg MSUALG_4:def 14 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds QuotMSAlg (U1,R) = MSAlgebra(# (Class R),(QuotCharact R) #);

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
cluster QuotMSAlg (U1,R) -> strict non-empty ;
coherence
( QuotMSAlg (U1,R) is strict & QuotMSAlg (U1,R) is non-empty ) by MSUALG_1:def 3;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
let s be SortSymbol of S;
func MSNat_Hom (U1,R,s) -> Function of ( the Sorts of U1 . s),((Class R) . s) means :Def15: :: MSUALG_4:def 15
 for x being set st x in the Sorts of U1 . s holds
it . x = Class ((R . s),x);
existence
ex b1 being Function of ( the Sorts of U1 . s),((Class R) . s) st
for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x)
proof end;
uniqueness
for b1, b2 being Function of ( the Sorts of U1 . s),((Class R) . s) st ( for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds
b2 . x = Class ((R . s),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines MSNat_Hom MSUALG_4:def 15 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for s being SortSymbol of S
for b5 being Function of ( the Sorts of U1 . s),((Class R) . s) holds
( b5 = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds
b5 . x = Class ((R . s),x) );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func MSNat_Hom (U1,R) -> ManySortedFunction of U1,(QuotMSAlg (U1,R)) means :Def16: :: MSUALG_4:def 16
 for s being SortSymbol of S holds it . s = MSNat_Hom (U1,R,s);
existence
ex b1 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st
for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st ( for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds b2 . s = MSNat_Hom (U1,R,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines MSNat_Hom MSUALG_4:def 16 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds
( b4 = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b4 . s = MSNat_Hom (U1,R,s) );

theorem :: MSUALG_4:3
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let s be SortSymbol of S;
func MSCng (F,s) -> Equivalence_Relation of ( the Sorts of U1 . s) means :Def17: :: MSUALG_4:def 17
 for x, y being Element of the Sorts of U1 . s holds
( [x,y] in it iff (F . s) . x = (F . s) . y );
existence
ex b1 being Equivalence_Relation of ( the Sorts of U1 . s) st
for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of ( the Sorts of U1 . s) st ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b2 iff (F . s) . x = (F . s) . y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines MSCng MSUALG_4:def 17 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S
for b6 being Equivalence_Relation of ( the Sorts of U1 . s) holds
( b6 = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b6 iff (F . s) . x = (F . s) . y ) );

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;
func MSCng F -> MSCongruence of U1 means :Def18: :: MSUALG_4:def 18
 for s being SortSymbol of S holds it . s = MSCng (F,s);
existence
ex b1 being MSCongruence of U1 st
for s being SortSymbol of S holds b1 . s = MSCng (F,s)
proof end;
uniqueness
for b1, b2 being MSCongruence of U1 st ( for s being SortSymbol of S holds b1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSCng (F,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines MSCng MSUALG_4:def 18 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b5 being MSCongruence of U1 holds
( b5 = MSCng F iff for s being SortSymbol of S holds b5 . s = MSCng (F,s) );

definition
let S be non empty non void ManySortedSign ;
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 ;
func MSHomQuot (F,s) -> Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) means :Def19: :: MSUALG_4:def 19
 for x being Element of the Sorts of U1 . s holds it . (Class ((MSCng (F,s)),x)) = (F . s) . x;
existence
ex b1 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x
proof end;
uniqueness
for b1, b2 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines MSHomQuot MSUALG_4:def 19 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S st F is_homomorphism U1,U2 holds
for b6 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds
( b6 = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (Class ((MSCng (F,s)),x)) = (F . s) . x );

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
func MSHomQuot F -> ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 means :Def20: :: MSUALG_4:def 20
 for s being SortSymbol of S holds it . s = MSHomQuot (F,s);
existence
ex b1 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st
for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st ( for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSHomQuot (F,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines MSHomQuot MSUALG_4:def 20 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for b5 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds
( b5 = MSHomQuot F iff for s being SortSymbol of S holds b5 . s = MSHomQuot (F,s) );

theorem Th4: :: MSUALG_4:4
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
proof end;

theorem Th5: :: MSUALG_4:5
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
proof end;

theorem :: MSUALG_4:6
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic
proof end;