begin
begin
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;
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)
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
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
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
end;
definition
let S be non
empty non
void ManySortedSign ;
let A be
non-empty MSAlgebra over
S;
let R be
MSCongruence of
A;
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)
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
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)
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
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;
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
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
end;
definition
let S be non
empty non
void ManySortedSign ;
let U1 be
non-empty MSAlgebra over
S;
let R be
MSCongruence of
U1;
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)
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
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;
assume A1:
F is_homomorphism U1,
U2
;
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
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
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;
existence
ex b1 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st
for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s)
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
end;