environ
vocabularies HIDDEN, UNIALG_1, SUBSET_1, NUMBERS, UNIALG_2, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, NAT_1, TARSKI, STRUCT_0, PARTFUN1, MSUALG_3, CQC_SIM1, WELLORD1, FINSEQ_2, GROUP_6, EQREL_1, FUNCT_2, CARD_3, RELAT_2, ALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FINSEQ_1, PARTFUN1, EQREL_1, FINSEQ_2, FUNCT_2, STRUCT_0, MARGREL1, UNIALG_1, FINSEQOP, FINSEQ_3, UNIALG_2;
definitions UNIALG_2, RELAT_2, TARSKI, FUNCT_1, XBOOLE_0, FUNCT_2, MARGREL1;
theorems FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, PARTFUN1, UNIALG_1, UNIALG_2, RELAT_1, RELSET_1, EQREL_1, ZFMISC_1, FINSEQ_3, XBOOLE_0, RELAT_2, ORDERS_1, MARGREL1;
schemes FINSEQ_1, RELSET_1, FUNCT_2, FUNCT_1;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, EQREL_1, FINSEQ_2, STRUCT_0, UNIALG_1, UNIALG_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1, MARGREL1;
constructors HIDDEN, EQREL_1, FINSEQOP, UNIALG_2, RELSET_1, CARD_3, FINSEQ_3, CARD_1, NAT_1, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET;
equalities UNIALG_2, XBOOLE_0;
expansions UNIALG_2, FUNCT_1, FUNCT_2, MARGREL1;
definition
let U1,
U2 be
Universal_Algebra;
let f be
Function of
U1,
U2;
assume A1:
f is_homomorphism
;
existence
ex b1 being Function of (QuotUnivAlg (U1,(Cng f))),U2 st
for a being Element of U1 holds b1 . (Class ((Cng f),a)) = f . a
uniqueness
for b1, b2 being Function of (QuotUnivAlg (U1,(Cng f))),U2 st ( for a being Element of U1 holds b1 . (Class ((Cng f),a)) = f . a ) & ( for a being Element of U1 holds b2 . (Class ((Cng f),a)) = f . a ) holds
b1 = b2
end;