:: MSUALG_4 semantic presentation

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

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

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

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

definition
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
mode ManySortedRelation of c2,c3 -> ManySortedSet of a1 means :Def2: :: MSUALG_4:def 2
for b1 being set st b1 in a1 holds
a4 . b1 is Relation of a2 . b1,a3 . b1;
existence
ex b1 being ManySortedSet of c1 st
for b2 being set st b2 in c1 holds
b1 . b2 is Relation of c2 . b2,c3 . b2
proof end;
end;

:: deftheorem Def2 defines ManySortedRelation MSUALG_4:def 2 :
for b1 being set
for b2, b3, b4 being ManySortedSet of b1 holds
( b4 is ManySortedRelation of b2,b3 iff for b5 being set st b5 in b1 holds
b4 . b5 is Relation of b2 . b5,b3 . b5 );

registration
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
cluster -> Relation-yielding ManySortedRelation of a2,a3;
coherence
for b1 being ManySortedRelation of c2,c3 holds b1 is Relation-yielding
proof end;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
mode ManySortedRelation of a2 is ManySortedRelation of a2,a2;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of c1;
let c3 be ManySortedRelation of c2;
attr a3 is MSEquivalence_Relation-like means :Def3: :: MSUALG_4:def 3
for b1 being set
for b2 being Relation of a2 . b1 st b1 in a1 & a3 . b1 = b2 holds
b2 is Equivalence_Relation of a2 . b1;
end;

:: deftheorem Def3 defines MSEquivalence_Relation-like MSUALG_4:def 3 :
for b1 being set
for b2 being ManySortedSet of b1
for b3 being ManySortedRelation of b2 holds
( b3 is MSEquivalence_Relation-like iff for b4 being set
for b5 being Relation of b2 . b4 st b4 in b1 & b3 . b4 = b5 holds
b5 is Equivalence_Relation of b2 . b4 );

definition
let c1 be non empty set ;
let c2, c3 be ManySortedSet of c1;
let c4 be ManySortedRelation of c2,c3;
let c5 be Element of c1;
redefine func . as c4 . c5 -> Relation of a2 . a5,a3 . a5;
coherence
c4 . c5 is Relation of c2 . c5,c3 . c5 by Def2;
end;

definition
let c1 be non empty ManySortedSign ;
let c2 be MSAlgebra of c1;
mode ManySortedRelation of a2 is ManySortedRelation of the Sorts of a2;
end;

definition
let c1 be non empty ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be ManySortedRelation of c2;
canceled;
attr a3 is MSEquivalence-like means :Def5: :: MSUALG_4:def 5
a3 is MSEquivalence_Relation-like;
end;

:: deftheorem Def4 MSUALG_4:def 4 :
canceled;

:: deftheorem Def5 defines MSEquivalence-like MSUALG_4:def 5 :
for b1 being non empty ManySortedSign
for b2 being MSAlgebra of b1
for b3 being ManySortedRelation of b2 holds
( b3 is MSEquivalence-like iff b3 is MSEquivalence_Relation-like );

registration
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
cluster MSEquivalence-like ManySortedRelation of the Sorts of a2,the Sorts of a2;
existence
ex b1 being ManySortedRelation of c2 st b1 is MSEquivalence-like
proof end;
end;

theorem Th1: :: MSUALG_4:1
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being SortSymbol of b1
for b4 being MSEquivalence-like ManySortedRelation of b2 holds b4 . b3 is Equivalence_Relation of the Sorts of b2 . b3
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSEquivalence-like ManySortedRelation of c2;
attr a3 is MSCongruence-like means :Def6: :: MSUALG_4:def 6
for b1 being OperSymbol of a1
for b2, b3 being Element of Args b1,a2 st ( for b4 being Nat st b4 in dom b2 holds
[(b2 . b4),(b3 . b4)] in a3 . ((the_arity_of b1) /. b4) ) holds
[((Den b1,a2) . b2),((Den b1,a2) . b3)] in a3 . (the_result_sort_of b1);
end;

:: deftheorem Def6 defines MSCongruence-like MSUALG_4:def 6 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSEquivalence-like ManySortedRelation of b2 holds
( b3 is MSCongruence-like iff for b4 being OperSymbol of b1
for b5, b6 being Element of Args b4,b2 st ( for b7 being Nat st b7 in dom b5 holds
[(b5 . b7),(b6 . b7)] in b3 . ((the_arity_of b4) /. b7) ) holds
[((Den b4,b2) . b5),((Den b4,b2) . b6)] in b3 . (the_result_sort_of b4) );

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
cluster MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of a2,the Sorts of a2;
existence
ex b1 being MSEquivalence-like ManySortedRelation of c2 st b1 is MSCongruence-like
proof end;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
mode MSCongruence of a2 is MSEquivalence-like MSCongruence-like ManySortedRelation of a2;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be MSEquivalence-like ManySortedRelation of c2;
let c4 be Element of c1;
redefine func . as c3 . c4 -> Equivalence_Relation of the Sorts of a2 . a4;
coherence
c3 . c4 is Equivalence_Relation of the Sorts of c2 . c4 by Th1;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be MSEquivalence-like ManySortedRelation of c2;
let c4 be Element of c1;
let c5 be Element of the Sorts of c2 . c4;
func Class c3,c5 -> Subset of (the Sorts of a2 . a4) equals :: MSUALG_4:def 7
 Class (a3 . a4),a5;
correctness
coherence
Class (c3 . c4),c5 is Subset of (the Sorts of c2 . c4);
;
end;

:: deftheorem Def7 defines Class MSUALG_4:def 7 :
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being MSEquivalence-like ManySortedRelation of b2
for b4 being Element of b1
for b5 being Element of the Sorts of b2 . b4 holds Class b3,b5 = Class (b3 . b4),b5;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
func Class c3 -> V2 ManySortedSet of the carrier of a1 means :Def8: :: MSUALG_4:def 8
for b1 being Element of a1 holds a4 . b1 = Class (a3 . b1);
existence
ex b1 being V2 ManySortedSet of the carrier of c1 st
for b2 being Element of c1 holds b1 . b2 = Class (c3 . b2)
proof end;
uniqueness
for b1, b2 being V2 ManySortedSet of the carrier of c1 st ( for b3 being Element of c1 holds b1 . b3 = Class (c3 . b3) ) & ( for b3 being Element of c1 holds b2 . b3 = Class (c3 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Class MSUALG_4:def 8 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being V2 ManySortedSet of the carrier of b1 holds
( b4 = Class b3 iff for b5 being Element of b1 holds b4 . b5 = Class (b3 . b5) );

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be ManySortedSet of the OperSymbols of c1;
let c4 be ManySortedFunction of c2,c3;
let c5 be OperSymbol of c1;
redefine func . as c4 . c5 -> Function of a2 . a5,a3 . a5;
coherence
c4 . c5 is Function of c2 . c5,c3 . c5
proof end;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be V2 ManySortedSet of c1;
redefine func * as c3 * c2 -> V2 ManySortedSet of dom a2;
coherence
c2 * c3 is V2 ManySortedSet of dom c2
proof end;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be non-empty MSAlgebra of c1;
let c4 be MSCongruence of c3;
let c5 be Element of Args c2,c3;
func c4 # c5 -> Element of product ((Class a4) * (the_arity_of a2)) means :Def9: :: MSUALG_4:def 9
for b1 being Nat st b1 in dom (the_arity_of a2) holds
a6 . b1 = Class (a4 . ((the_arity_of a2) /. b1)),(a5 . b1);
existence
ex b1 being Element of product ((Class c4) * (the_arity_of c2)) st
for b2 being Nat st b2 in dom (the_arity_of c2) holds
b1 . b2 = Class (c4 . ((the_arity_of c2) /. b2)),(c5 . b2)
proof end;
uniqueness
for b1, b2 being Element of product ((Class c4) * (the_arity_of c2)) st ( for b3 being Nat st b3 in dom (the_arity_of c2) holds
b1 . b3 = Class (c4 . ((the_arity_of c2) /. b3)),(c5 . b3) ) & ( for b3 being Nat st b3 in dom (the_arity_of c2) holds
b2 . b3 = Class (c4 . ((the_arity_of c2) /. b3)),(c5 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines # MSUALG_4:def 9 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1
for b4 being MSCongruence of b3
for b5 being Element of Args b2,b3
for b6 being Element of product ((Class b4) * (the_arity_of b2)) holds
( b6 = b4 # b5 iff for b7 being Nat st b7 in dom (the_arity_of b2) holds
b6 . b7 = Class (b4 . ((the_arity_of b2) /. b7)),(b5 . b7) );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be non-empty MSAlgebra of c1;
let c4 be MSCongruence of c3;
func QuotRes c4,c2 -> Function of (the Sorts of a3 * the ResultSort of a1) . a2,((Class a4) * the ResultSort of a1) . a2 means :Def10: :: MSUALG_4:def 10
for b1 being Element of the Sorts of a3 . (the_result_sort_of a2) holds a5 . b1 = Class a4,b1;
existence
ex b1 being Function of (the Sorts of c3 * the ResultSort of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st
for b2 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b1 . b2 = Class c4,b2
proof end;
uniqueness
for b1, b2 being Function of (the Sorts of c3 * the ResultSort of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st ( for b3 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b1 . b3 = Class c4,b3 ) & ( for b3 being Element of the Sorts of c3 . (the_result_sort_of c2) holds b2 . b3 = Class c4,b3 ) holds
b1 = b2
proof end;
func QuotArgs c4,c2 -> Function of ((the Sorts of a3 # ) * the Arity of a1) . a2,(((Class a4) # ) * the Arity of a1) . a2 means :: MSUALG_4:def 11
for b1 being Element of Args a2,a3 holds a5 . b1 = a4 # b1;
existence
ex b1 being Function of ((the Sorts of c3 # ) * the Arity of c1) . c2,(((Class c4) # ) * the Arity of c1) . c2 st
for b2 being Element of Args c2,c3 holds b1 . b2 = c4 # b2
proof end;
uniqueness
for b1, b2 being Function of ((the Sorts of c3 # ) * the Arity of c1) . c2,(((Class c4) # ) * the Arity of c1) . c2 st ( for b3 being Element of Args c2,c3 holds b1 . b3 = c4 # b3 ) & ( for b3 being Element of Args c2,c3 holds b2 . b3 = c4 # b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines QuotRes MSUALG_4:def 10 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1
for b4 being MSCongruence of b3
for b5 being Function of (the Sorts of b3 * the ResultSort of b1) . b2,((Class b4) * the ResultSort of b1) . b2 holds
( b5 = QuotRes b4,b2 iff for b6 being Element of the Sorts of b3 . (the_result_sort_of b2) holds b5 . b6 = Class b4,b6 );

:: deftheorem Def11 defines QuotArgs MSUALG_4:def 11 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1
for b4 being MSCongruence of b3
for b5 being Function of ((the Sorts of b3 # ) * the Arity of b1) . b2,(((Class b4) # ) * the Arity of b1) . b2 holds
( b5 = QuotArgs b4,b2 iff for b6 being Element of Args b2,b3 holds b5 . b6 = b4 # b6 );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
func QuotRes c3 -> ManySortedFunction of the Sorts of a2 * the ResultSort of a1,(Class a3) * the ResultSort of a1 means :: MSUALG_4:def 12
for b1 being OperSymbol of a1 holds a4 . b1 = QuotRes a3,b1;
existence
ex b1 being ManySortedFunction of the Sorts of c2 * the ResultSort of c1,(Class c3) * the ResultSort of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = QuotRes c3,b2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of the Sorts of c2 * the ResultSort of c1,(Class c3) * the ResultSort of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = QuotRes c3,b3 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = QuotRes c3,b3 ) holds
b1 = b2
proof end;
func QuotArgs c3 -> ManySortedFunction of (the Sorts of a2 # ) * the Arity of a1,((Class a3) # ) * the Arity of a1 means :: MSUALG_4:def 13
for b1 being OperSymbol of a1 holds a4 . b1 = QuotArgs a3,b1;
existence
ex b1 being ManySortedFunction of (the Sorts of c2 # ) * the Arity of c1,((Class c3) # ) * the Arity of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = QuotArgs c3,b2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (the Sorts of c2 # ) * the Arity of c1,((Class c3) # ) * the Arity of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = QuotArgs c3,b3 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = QuotArgs c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines QuotRes MSUALG_4:def 12 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being ManySortedFunction of the Sorts of b2 * the ResultSort of b1,(Class b3) * the ResultSort of b1 holds
( b4 = QuotRes b3 iff for b5 being OperSymbol of b1 holds b4 . b5 = QuotRes b3,b5 );

:: deftheorem Def13 defines QuotArgs MSUALG_4:def 13 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being ManySortedFunction of (the Sorts of b2 # ) * the Arity of b1,((Class b3) # ) * the Arity of b1 holds
( b4 = QuotArgs b3 iff for b5 being OperSymbol of b1 holds b4 . b5 = QuotArgs b3,b5 );

theorem Th2: :: MSUALG_4:2
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1
for b4 being MSCongruence of b3
for b5 being set st b5 in (((Class b4) # ) * the Arity of b1) . b2 holds
ex b6 being Element of Args b2,b3 st b5 = b4 # b6
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be non-empty MSAlgebra of c1;
let c4 be MSCongruence of c3;
func QuotCharact c4,c2 -> Function of (((Class a4) # ) * the Arity of a1) . a2,((Class a4) * the ResultSort of a1) . a2 means :Def14: :: MSUALG_4:def 14
for b1 being Element of Args a2,a3 st a4 # b1 in (((Class a4) # ) * the Arity of a1) . a2 holds
a5 . (a4 # b1) = ((QuotRes a4,a2) * (Den a2,a3)) . b1;
existence
ex b1 being Function of (((Class c4) # ) * the Arity of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st
for b2 being Element of Args c2,c3 st c4 # b2 in (((Class c4) # ) * the Arity of c1) . c2 holds
b1 . (c4 # b2) = ((QuotRes c4,c2) * (Den c2,c3)) . b2
proof end;
uniqueness
for b1, b2 being Function of (((Class c4) # ) * the Arity of c1) . c2,((Class c4) * the ResultSort of c1) . c2 st ( for b3 being Element of Args c2,c3 st c4 # b3 in (((Class c4) # ) * the Arity of c1) . c2 holds
b1 . (c4 # b3) = ((QuotRes c4,c2) * (Den c2,c3)) . b3 ) & ( for b3 being Element of Args c2,c3 st c4 # b3 in (((Class c4) # ) * the Arity of c1) . c2 holds
b2 . (c4 # b3) = ((QuotRes c4,c2) * (Den c2,c3)) . b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines QuotCharact MSUALG_4:def 14 :
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty MSAlgebra of b1
for b4 being MSCongruence of b3
for b5 being Function of (((Class b4) # ) * the Arity of b1) . b2,((Class b4) * the ResultSort of b1) . b2 holds
( b5 = QuotCharact b4,b2 iff for b6 being Element of Args b2,b3 st b4 # b6 in (((Class b4) # ) * the Arity of b1) . b2 holds
b5 . (b4 # b6) = ((QuotRes b4,b2) * (Den b2,b3)) . b6 );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
func QuotCharact c3 -> ManySortedFunction of ((Class a3) # ) * the Arity of a1,(Class a3) * the ResultSort of a1 means :Def15: :: MSUALG_4:def 15
for b1 being OperSymbol of a1 holds a4 . b1 = QuotCharact a3,b1;
existence
ex b1 being ManySortedFunction of ((Class c3) # ) * the Arity of c1,(Class c3) * the ResultSort of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = QuotCharact c3,b2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((Class c3) # ) * the Arity of c1,(Class c3) * the ResultSort of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = QuotCharact c3,b3 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = QuotCharact c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines QuotCharact MSUALG_4:def 15 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being ManySortedFunction of ((Class b3) # ) * the Arity of b1,(Class b3) * the ResultSort of b1 holds
( b4 = QuotCharact b3 iff for b5 being OperSymbol of b1 holds b4 . b5 = QuotCharact b3,b5 );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
func QuotMSAlg c2,c3 -> MSAlgebra of a1 equals :: MSUALG_4:def 16
 MSAlgebra(# (Class a3),(QuotCharact a3) #);
coherence
MSAlgebra(# (Class c3),(QuotCharact c3) #) is MSAlgebra of c1 ;
end;

:: deftheorem Def16 defines QuotMSAlg MSUALG_4:def 16 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2 holds QuotMSAlg b2,b3 = MSAlgebra(# (Class b3),(QuotCharact b3) #);

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
cluster QuotMSAlg a2,a3 -> strict non-empty ;
coherence
( QuotMSAlg c2,c3 is strict & QuotMSAlg c2,c3 is non-empty ) by MSUALG_1:def 8;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
let c4 be SortSymbol of c1;
func MSNat_Hom c2,c3,c4 -> Function of the Sorts of a2 . a4,(Class a3) . a4 means :Def17: :: MSUALG_4:def 17
for b1 being set st b1 in the Sorts of a2 . a4 holds
a5 . b1 = Class (a3 . a4),b1;
existence
ex b1 being Function of the Sorts of c2 . c4,(Class c3) . c4 st
for b2 being set st b2 in the Sorts of c2 . c4 holds
b1 . b2 = Class (c3 . c4),b2
proof end;
uniqueness
for b1, b2 being Function of the Sorts of c2 . c4,(Class c3) . c4 st ( for b3 being set st b3 in the Sorts of c2 . c4 holds
b1 . b3 = Class (c3 . c4),b3 ) & ( for b3 being set st b3 in the Sorts of c2 . c4 holds
b2 . b3 = Class (c3 . c4),b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines MSNat_Hom MSUALG_4:def 17 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being SortSymbol of b1
for b5 being Function of the Sorts of b2 . b4,(Class b3) . b4 holds
( b5 = MSNat_Hom b2,b3,b4 iff for b6 being set st b6 in the Sorts of b2 . b4 holds
b5 . b6 = Class (b3 . b4),b6 );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be MSCongruence of c2;
func MSNat_Hom c2,c3 -> ManySortedFunction of a2,(QuotMSAlg a2,a3) means :Def18: :: MSUALG_4:def 18
for b1 being SortSymbol of a1 holds a4 . b1 = MSNat_Hom a2,a3,b1;
existence
ex b1 being ManySortedFunction of c2,(QuotMSAlg c2,c3) st
for b2 being SortSymbol of c1 holds b1 . b2 = MSNat_Hom c2,c3,b2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of c2,(QuotMSAlg c2,c3) st ( for b3 being SortSymbol of c1 holds b1 . b3 = MSNat_Hom c2,c3,b3 ) & ( for b3 being SortSymbol of c1 holds b2 . b3 = MSNat_Hom c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines MSNat_Hom MSUALG_4:def 18 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2
for b4 being ManySortedFunction of b2,(QuotMSAlg b2,b3) holds
( b4 = MSNat_Hom b2,b3 iff for b5 being SortSymbol of b1 holds b4 . b5 = MSNat_Hom b2,b3,b5 );

theorem Th3: :: MSUALG_4:3
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being MSCongruence of b2 holds MSNat_Hom b2,b3 is_epimorphism b2, QuotMSAlg b2,b3
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
let c5 be SortSymbol of c1;
func MSCng c4,c5 -> Equivalence_Relation of the Sorts of a2 . a5 means :Def19: :: MSUALG_4:def 19
for b1, b2 being Element of the Sorts of a2 . a5 holds
( [b1,b2] in a6 iff (a4 . a5) . b1 = (a4 . a5) . b2 );
existence
ex b1 being Equivalence_Relation of the Sorts of c2 . c5 st
for b2, b3 being Element of the Sorts of c2 . c5 holds
( [b2,b3] in b1 iff (c4 . c5) . b2 = (c4 . c5) . b3 )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of the Sorts of c2 . c5 st ( for b3, b4 being Element of the Sorts of c2 . c5 holds
( [b3,b4] in b1 iff (c4 . c5) . b3 = (c4 . c5) . b4 ) ) & ( for b3, b4 being Element of the Sorts of c2 . c5 holds
( [b3,b4] in b2 iff (c4 . c5) . b3 = (c4 . c5) . b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines MSCng MSUALG_4:def 19 :
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3
for b5 being SortSymbol of b1
for b6 being Equivalence_Relation of the Sorts of b2 . b5 holds
( b6 = MSCng b4,b5 iff for b7, b8 being Element of the Sorts of b2 . b5 holds
( [b7,b8] in b6 iff (b4 . b5) . b7 = (b4 . b5) . b8 ) );

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
assume E16: c4 is_homomorphism c2,c3 ;
func MSCng c4 -> MSCongruence of a2 means :Def20: :: MSUALG_4:def 20
for b1 being SortSymbol of a1 holds a5 . b1 = MSCng a4,b1;
existence
ex b1 being MSCongruence of c2 st
for b2 being SortSymbol of c1 holds b1 . b2 = MSCng c4,b2
proof end;
uniqueness
for b1, b2 being MSCongruence of c2 st ( for b3 being SortSymbol of c1 holds b1 . b3 = MSCng c4,b3 ) & ( for b3 being SortSymbol of c1 holds b2 . b3 = MSCng c4,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines MSCng MSUALG_4:def 20 :
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
for b5 being MSCongruence of b2 holds
( b5 = MSCng b4 iff for b6 being SortSymbol of b1 holds b5 . b6 = MSCng b4,b6 );

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
let c5 be SortSymbol of c1;
assume E17: c4 is_homomorphism c2,c3 ;
func MSHomQuot c4,c5 -> Function of the Sorts of (QuotMSAlg a2,(MSCng a4)) . a5,the Sorts of a3 . a5 means :Def21: :: MSUALG_4:def 21
for b1 being Element of the Sorts of a2 . a5 holds a6 . (Class (MSCng a4,a5),b1) = (a4 . a5) . b1;
existence
ex b1 being Function of the Sorts of (QuotMSAlg c2,(MSCng c4)) . c5,the Sorts of c3 . c5 st
for b2 being Element of the Sorts of c2 . c5 holds b1 . (Class (MSCng c4,c5),b2) = (c4 . c5) . b2
proof end;
uniqueness
for b1, b2 being Function of the Sorts of (QuotMSAlg c2,(MSCng c4)) . c5,the Sorts of c3 . c5 st ( for b3 being Element of the Sorts of c2 . c5 holds b1 . (Class (MSCng c4,c5),b3) = (c4 . c5) . b3 ) & ( for b3 being Element of the Sorts of c2 . c5 holds b2 . (Class (MSCng c4,c5),b3) = (c4 . c5) . b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines MSHomQuot MSUALG_4:def 21 :
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3
for b5 being SortSymbol of b1 st b4 is_homomorphism b2,b3 holds
for b6 being Function of the Sorts of (QuotMSAlg b2,(MSCng b4)) . b5,the Sorts of b3 . b5 holds
( b6 = MSHomQuot b4,b5 iff for b7 being Element of the Sorts of b2 . b5 holds b6 . (Class (MSCng b4,b5),b7) = (b4 . b5) . b7 );

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,c3;
func MSHomQuot c4 -> ManySortedFunction of (QuotMSAlg a2,(MSCng a4)),a3 means :Def22: :: MSUALG_4:def 22
for b1 being SortSymbol of a1 holds a5 . b1 = MSHomQuot a4,b1;
existence
ex b1 being ManySortedFunction of (QuotMSAlg c2,(MSCng c4)),c3 st
for b2 being SortSymbol of c1 holds b1 . b2 = MSHomQuot c4,b2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotMSAlg c2,(MSCng c4)),c3 st ( for b3 being SortSymbol of c1 holds b1 . b3 = MSHomQuot c4,b3 ) & ( for b3 being SortSymbol of c1 holds b2 . b3 = MSHomQuot c4,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines MSHomQuot MSUALG_4:def 22 :
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3
for b5 being ManySortedFunction of (QuotMSAlg b2,(MSCng b4)),b3 holds
( b5 = MSHomQuot b4 iff for b6 being SortSymbol of b1 holds b5 . b6 = MSHomQuot b4,b6 );

theorem Th4: :: MSUALG_4:4
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 holds
MSHomQuot b4 is_monomorphism QuotMSAlg b2,(MSCng b4),b3
proof end;

theorem Th5: :: MSUALG_4:5
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_epimorphism b2,b3 holds
MSHomQuot b4 is_isomorphism QuotMSAlg b2,(MSCng b4),b3
proof end;

theorem Th6: :: MSUALG_4:6
for b1 being non empty non void ManySortedSign
for b2, b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_epimorphism b2,b3 holds
QuotMSAlg b2,(MSCng b4),b3 are_isomorphic
proof end;