environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, ALTCAT_1, ALTCAT_2, MSUALG_6, FUNCTOR0, RELAT_1, FUNCT_2, FUNCT_1, SUBSET_1, FUNCT_3, ZFMISC_1, STRUCT_0, TARSKI, MEMBER_1, MSUALG_3, ENS_1, CAT_1, PBOOLE, REALSET1, PZFMISC1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, BINOP_1, REALSET1, PZFMISC1, STRUCT_0, MSUALG_3, ALTCAT_1, ALTCAT_2, FUNCT_3, FUNCTOR0;
definitions TARSKI, PBOOLE, MSUALG_3, ALTCAT_2, FUNCTOR0, PZFMISC1;
theorems ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE, RELAT_1, MSUALG_3, XBOOLE_1, PARTFUN1;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_2, FUNCTOR0, RELSET_1;
constructors HIDDEN, REALSET1, PZFMISC1, MSUALG_3, FUNCTOR0, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCTOR0, BINOP_1, REALSET1;
expansions PBOOLE, MSUALG_3, ALTCAT_2, FUNCTOR0, PZFMISC1;
Lm1:
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
:: Lemmata about properties of G*F, where G,F are FunctorStr
:: ===================================================================