environ
vocabularies HIDDEN, UNIALG_1, FUNCT_2, STRUCT_0, FUNCT_1, MSUALG_3, SUBSET_1, RELAT_1, XBOOLE_0, TARSKI, BINOP_1, ALGSTR_0, MESFUNC1, VECTSP_1, GROUP_1, MSUALG_1, AUTALG_1, PBOOLE, MEMBER_1, CARD_1, FUNCOP_1, MSUHOM_1, MSSUBFAM, GROUP_6, WELLORD1, ZFMISC_1, ENDALG;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, CARD_3, BINOP_1, PARTFUN1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, FINSEQ_1, PZFMISC1, UNIALG_1, MSUALG_1, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, GROUP_6;
definitions FUNCT_1, TARSKI, VECTSP_1, GROUP_1, FUNCT_2;
theorems AUTALG_1, ALG_1, BINOP_1, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_6, MSUALG_1, MSUALG_3, MSUHOM_1, TARSKI, ZFMISC_1, RELAT_1, VECTSP_1, RELSET_1, XBOOLE_0, GROUP_1, PBOOLE;
schemes BINOP_1, FUNCT_1, XBOOLE_0;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, VECTSP_1, MSUALG_1, ALGSTR_0, RELSET_1;
constructors HIDDEN, BINOP_1, CARD_3, PZFMISC1, VECTSP_1, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCOP_1, STRUCT_0, ALGSTR_0;
expansions TARSKI, GROUP_1, FUNCT_2;
definition
let S be non
empty non
void ManySortedSign ;
let U1 be
non-empty MSAlgebra over
S;
set T = the
Sorts of
U1;
existence
ex b1 being MSFunctionSet of U1,U1 st
( ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) )
uniqueness
for b1, b2 being MSFunctionSet of U1,U1 st ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in b2 iff h is_homomorphism U1,U1 ) ) holds
b1 = b2
end;
Lm3:
for UA being Universal_Algebra
for h being Function st dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds
h . x = 0 .--> x ) holds
rng h = MSAEnd (MSAlg UA)