environ
vocabularies HIDDEN, STRUCT_0, GROUP_1, GROUP_2, SUBSET_1, GROUP_6, NEWTON, PRE_TOPC, RELAT_1, TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, BINOP_1, ALGSTR_0, ZFMISC_1, REALSET1, GROUP_5, WELLORD1, AUTGROUP;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0, BINOP_1, GROUP_1, GROUP_2, GROUP_3, GROUP_5, GROUP_6;
definitions FUNCT_1, TARSKI, FUNCT_2;
theorems FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, GROUP_5, GROUP_6, REALSET1, RELAT_1, ZFMISC_1, XBOOLE_0, STRUCT_0;
schemes BINOP_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_2;
constructors HIDDEN, BINOP_1, REALSET1, GROUP_5, GROUP_6, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, REALSET1, GROUP_2, GROUP_3, ALGSTR_0;
expansions BINOP_1, FUNCT_2;
Lm1:
for G being strict Group
for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
Lm2:
for G being strict Group
for H being Subgroup of G st H is normal holds
for a, b being Element of G st b is Element of H holds
b |^ a in H
Lm3:
for G being strict Group
for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )