environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, TARSKI, NUMBERS, INT_1, GROUP_1, GROUP_2, PRE_TOPC, FINSEQ_1, STRUCT_0, NEWTON, RELAT_1, EQREL_1, BINOP_1, NAT_1, FUNCT_1, PARTFUN1, ORDINAL4, ARYTM_3, CARD_1, CARD_3, QC_LANG1, XXREAL_1, ARYTM_1, GROUP_4, RLSUB_1, FINSET_1, CQC_SIM1, GROUP_3, GROUP_5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, PARTFUN1, CARD_1, FINSEQ_1, FINSET_1, FINSEQ_4, INT_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4;
definitions TARSKI, GROUP_1, XBOOLE_0;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, GROUP_1, GROUP_2, GROUP_3, GROUP_4, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, CARD_2, FINSOP_1, STRUCT_0, PARTFUN1;
schemes FINSEQ_2, DOMAIN_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, ORDINAL1, FINSEQ_1, CARD_1;
constructors HIDDEN, PARTFUN1, SETFAM_1, NAT_1, FINSEQ_4, FINSOP_1, REALSET1, GROUP_4, RELSET_1, BINOP_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities XBOOLE_0, GROUP_2, GROUP_3, GROUP_4;
expansions TARSKI, GROUP_1, GROUP_3;
Lm1:
for G being commutative Group
for a, b being Element of G holds a * b = b * a
;
Lm2:
for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
:: P. Hall Identity.
::