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


definition
let IT be Function;
attr IT is Relation-yielding means :Def1: :: MSUALG_4:def 1
for x being set st x in dom IT holds
IT . x is Relation;
end;

:: deftheorem Def1 defines Relation-yielding MSUALG_4:def 1 :
for IT being Function holds
( IT is Relation-yielding iff for x being set st x in dom IT holds
IT . x is Relation );

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

definition
let I be set ;
mode ManySortedRelation of I is Relation-yielding ManySortedSet of I;
end;

definition
let I be set ;
let A, B be ManySortedSet of I;
mode ManySortedRelation of A,B -> ManySortedSet of I means :Def2: :: MSUALG_4:def 2
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 Def2 defines ManySortedRelation MSUALG_4:def 2 :
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 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 :Def3: :: MSUALG_4:def 3
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 Def3 defines MSEquivalence_Relation-like MSUALG_4:def 3 :
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 Def2;
end;

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

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

:: deftheorem MSUALG_4:def 4 :
canceled;

:: deftheorem Def5 defines MSEquivalence-like MSUALG_4:def 5 :
for S being non empty ManySortedSign
for U1 being MSAlgebra of 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 of S;
cluster MSEquivalence-like 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 of 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
proof end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
let R be MSEquivalence-like ManySortedRelation of U1;
attr R is MSCongruence-like means :Def6: :: MSUALG_4:def 6
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 Def6 defines MSCongruence-like MSUALG_4:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 of S;
cluster MSEquivalence-like MSCongruence-like 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 of 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 of 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 of 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 7
 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 7 :
for S being non empty non void ManySortedSign
for U1 being MSAlgebra of 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 of S;
let R be MSCongruence of U1;
func Class R -> V5 ManySortedSet of the carrier of S means :Def8: :: MSUALG_4:def 8
for s being Element of S holds it . s = Class (R . s);
existence
ex b1 being V5 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 V5 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 Def8 defines Class MSUALG_4:def 8 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1
for b4 being V5 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 18;
end;

definition
let I be non empty set ;
let p be FinSequence of I;
let X be ManySortedSet of I;
:: original: *
redefine func X * p -> ManySortedSet of dom p;
coherence
p * X is ManySortedSet of dom p
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra of 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 :Def9: :: MSUALG_4:def 9
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 Def9 defines # MSUALG_4:def 9 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of 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 of 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 :Def10: :: MSUALG_4:def 10
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 11
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 Def10 defines QuotRes MSUALG_4:def 10 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of 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 11 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of 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 of 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 12
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 13
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 12 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 13 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 of 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 of 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 :Def14: :: MSUALG_4:def 14
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 Def14 defines QuotCharact MSUALG_4:def 14 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra of 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 of 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 :Def15: :: MSUALG_4:def 15
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 Def15 defines QuotCharact MSUALG_4:def 15 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 of S;
let R be MSCongruence of U1;
func QuotMSAlg U1,R -> MSAlgebra of S equals :: MSUALG_4:def 16
 MSAlgebra(# (Class R),(QuotCharact R) #);
coherence
MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra of S ;
end;

:: deftheorem defines QuotMSAlg MSUALG_4:def 16 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 of 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 8;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra of 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 :Def17: :: MSUALG_4:def 17
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 Def17 defines MSNat_Hom MSUALG_4:def 17 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 of S;
let R be MSCongruence of U1;
func MSNat_Hom U1,R -> ManySortedFunction of U1,(QuotMSAlg U1,R) means :Def18: :: MSUALG_4:def 18
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 Def18 defines MSNat_Hom MSUALG_4:def 18 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of 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 of 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 of 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 :Def19: :: MSUALG_4:def 19
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 Def19 defines MSCng MSUALG_4:def 19 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;
func MSCng F -> MSCongruence of U1 means :Def20: :: MSUALG_4:def 20
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 Def20 defines MSCng MSUALG_4:def 20 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of 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 :Def21: :: MSUALG_4:def 21
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 Def21 defines MSHomQuot MSUALG_4:def 21 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of S;
let F be ManySortedFunction of U1,U2;
func MSHomQuot F -> ManySortedFunction of (QuotMSAlg U1,(MSCng F)),U2 means :Def22: :: MSUALG_4:def 22
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 Def22 defines MSHomQuot MSUALG_4:def 22 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of 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 of 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 of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg U1,(MSCng F),U2 are_isomorphic
proof end;