environ
vocabularies HIDDEN, GROUP_1, SUBSET_1, GROUP_2, NAT_1, INT_1, RELAT_1, BINOP_1, ALGSTR_0, FUNCT_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FINSET_1, CARD_1, NEWTON, ARYTM_3, XXREAL_0, COMPLEX1, RLSUB_1, CQC_SIM1, SETFAM_1, PRE_TOPC, GROUP_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, CARD_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, DOMAIN_1, XXREAL_0, INT_1, INT_2;
definitions XBOOLE_0, BINOP_1, FUNCT_1, GROUP_2, TARSKI, GROUP_1;
theorems ABSVALUE, CARD_1, CARD_2, ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, STRUCT_0, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, NAT_1, SUBSET_1, XBOOLE_0, CLASSES1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, ORDINAL1;
constructors HIDDEN, SETFAM_1, WELLORD2, BINOP_1, XXREAL_0, NAT_1, INT_2, REALSET1, REAL_1, GROUP_2, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities BINOP_1, GROUP_2, TARSKI, ALGSTR_0, STRUCT_0;
expansions XBOOLE_0, BINOP_1, GROUP_1, STRUCT_0;
theorem Th1:
for
G being
Group for
a,
b being
Element of
G holds
(
(a * b) * (b ") = a &
(a * (b ")) * b = a &
((b ") * b) * a = a &
(b * (b ")) * a = a &
a * (b * (b ")) = a &
a * ((b ") * b) = a &
(b ") * (b * a) = a &
b * ((b ") * a) = a )
Lm1:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
Lm4:
for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n
Lm5:
for G being Group
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) * (carr N2) c= (carr N2) * (carr N1)