environ
vocabularies HIDDEN, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7, FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, CARD_3, ORDINAL1, NUMBERS, FINSEQ_1, XXREAL_0, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GROUP_7, FUNCT_7;
definitions ;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, TARSKI, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, FINSEQ_2, XREAL_1, ORDINAL1, FINSEQ_1, FINSEQ_3, NAT_1, XBOOLE_0, RELAT_1, XXREAL_0, GROUP_7, FUNCT_7, YELLOW17, STRUCT_0, PARTFUN1;
schemes NAT_1, SUBSET_1, FUNCT_2, FINSEQ_1, XFAMILY;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, FUNCOP_1, CARD_1, CARD_3, GROUP_7, XXREAL_0, RELSET_1, FINSEQ_1;
constructors HIDDEN, BINOP_1, REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4, GROUP_7, FUNCT_7, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1;
expansions FINSEQ_1;
Lm1:
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )