environ
vocabularies HIDDEN, STRUCT_0, XBOOLE_0, MSUALG_1, FUNCT_1, RELAT_1, PBOOLE, FUNCOP_1, EQREL_1, SUBSET_1, NAT_1, MARGREL1, PARTFUN1, FINSEQ_1, TARSKI, CARD_3, MSUALG_3, WELLORD1, MSUALG_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1, STRUCT_0, ORDINAL1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3, PBOOLE, FUNCOP_1, MSUALG_1, MSUALG_3;
definitions TARSKI, MSUALG_3, XBOOLE_0, FUNCOP_1;
theorems FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, MSUALG_3, MSAFREE, XBOOLE_0, FUNCOP_1, ORDINAL1, PARTFUN1, FINSEQ_2;
schemes FUNCT_1, CLASSES1, EQREL_1;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, CARD_3, RELSET_1, FINSEQ_2, FINSEQ_1;
constructors HIDDEN, EQREL_1, PRALG_2, MSUALG_3, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0;
expansions TARSKI, MSUALG_3, XBOOLE_0, FUNCOP_1;
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;