environ
vocabularies HIDDEN, UNIALG_1, FUNCT_1, RELAT_1, STRUCT_0, MSUALG_3, FUNCT_2, SUBSET_1, XBOOLE_0, TARSKI, BINOP_1, GROUP_1, ALGSTR_0, PBOOLE, PZFMISC1, FUNCOP_1, MEMBER_1, MSUALG_1, CARD_3, CARD_1, MSUHOM_1, CQC_SIM1, GROUP_6, ZFMISC_1, WELLORD1, AUTALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, STRUCT_0, ALGSTR_0, FINSEQ_1, BINOP_1, GROUP_1, GROUP_6, CARD_3, PZFMISC1, UNIALG_1, UNIALG_2, ALG_1, MSUALG_1, MSUALG_3, MSUHOM_1;
definitions FUNCT_1, ALG_1, GROUP_6, MSUALG_3, TARSKI, XBOOLE_0, PZFMISC1, FUNCT_2;
theorems ALG_1, BINOP_1, CARD_3, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_6, MSUALG_1, MSUALG_3, MSUHOM_1, PBOOLE, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0, PARTFUN1;
schemes BINOP_1, FUNCT_1, XBOOLE_0;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, SUBSET_1;
constructors HIDDEN, BINOP_1, CARD_3, PZFMISC1, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1, RELSET_1, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET;
equalities FUNCOP_1, ALGSTR_0;
expansions ALG_1, MSUALG_3, TARSKI, XBOOLE_0, PZFMISC1, FUNCT_2;
Lm1:
for UA being Universal_Algebra
for f being Function of UA,UA st f is_isomorphism holds
f " is Function of UA,UA
Lm2:
for UA being Universal_Algebra
for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
Lm3:
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for f being Element of MSAAut U1 holds
( f is "1-1" & f is "onto" )
Lm4:
for UA being Universal_Algebra
for h being Function st dom h = UAAut UA & ( for x being object st x in UAAut UA holds
h . x = 0 .--> x ) holds
rng h = MSAAut (MSAlg UA)