environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FINSET_1, NAT_1, GROUP_1, RELAT_1, TARSKI, ALGSTR_0, BINOP_1, REALSET1, ZFMISC_1, FUNCT_1, RLSUB_1, CARD_1, XXREAL_0, NEWTON, SETFAM_1, CQC_SIM1, FINSUB_1, SETWISEO, ARYTM_3, GROUP_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSUB_1, FINSET_1, REALSET1, XCMPLX_0, XXREAL_0, CARD_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0, GROUP_1, WELLORD2, BINOP_1, SETWISEO, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, NAT_D, MCART_1;
definitions FUNCT_1, GROUP_1, STRUCT_0, TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSET_1, FINSUB_1, FUNCT_1, FUNCT_2, GROUP_1, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, NAT_D, STRUCT_0, NAT_1;
schemes FUNCT_1, SUBSET_1, SETWISEO, CLASSES1;
registrations SUBSET_1, RELSET_1, FINSET_1, FINSUB_1, MEMBERED, REALSET1, STRUCT_0, GROUP_1, ALGSTR_0, CARD_1, ORDINAL1, XCMPLX_0;
constructors HIDDEN, SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, MEMBERED, REALSET1, GROUP_1, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, XBOOLE_0, BINOP_1, REALSET1, SUBSET_1, ALGSTR_0;
expansions GROUP_1, STRUCT_0, TARSKI, XBOOLE_0;
Lm1:
for x being object
for G being non empty 1-sorted
for A being Subset of G st x in A holds
x is Element of G
;
Lm2:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
Lm3:
for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )
Lm4:
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
Lm5:
for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )