environ
vocabularies HIDDEN, GROUP_18, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, XXREAL_0, GROUP_2, GROUP_3, LOPBAN_1, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7, POWER, FUNCOP_1, ALGSTR_0, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, INT_2, PBOOLE, NEWTON, INT_1, GROUP_4, CQC_SIM1, REAL_1, XCMPLX_0, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, INT_2, FINSEQ_1, SEQ_4, POWER, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_5, GROUP_6, PRALG_1, GROUP_7, GROUP_17;
definitions TARSKI;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2, GROUP_3, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_5, GROUP_6, XREAL_1, ORDINAL1, NAT_1, INT_1, XCMPLX_1, GR_CY_2, XBOOLE_0, RELAT_1, XXREAL_0, GROUP_7, STRUCT_0, XBOOLE_1, NEWTON, NUMBERS, GROUPP_1, PARTFUN1, INT_2, NAT_D, ZFMISC_1, GR_CY_1, CARD_1, WELLORD2, GROUP_17, POWER, SEQ_4;
schemes NAT_1, FRAENKEL;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, FUNCOP_1, GROUP_7, GROUP_3, XXREAL_0, RELSET_1, FINSEQ_1, INT_1, GR_CY_1, FINSET_1, NAT_3, FUNCT_1, XCMPLX_0, MEMBERED, NEWTON, VALUED_0, XXREAL_2, FINSEQ_2, PBOOLE, GROUP_6, POWER;
constructors HIDDEN, REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4, GROUP_5, GROUP_7, RELSET_1, WELLORD2, NAT_D, NAT_3, SEQ_4, GROUP_17, POWER;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, GROUP_6, FINSEQ_1, STRUCT_0, FUNCOP_1, ORDINAL1;
expansions STRUCT_0;
LM204K1:
for p being Prime
for m, k being Nat st m divides p |^ k & m <> 1 holds
ex j being Nat st m = p |^ (j + 1)
LM204A:
for G being finite strict commutative Group
for p being Prime
for m being Nat
for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )
XLM18Th401:
for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for x being set st x in the carrier of (product F) holds
x is b1 -defined total Function
XLM18Th402:
for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for f being Function st f in the carrier of (product F) holds
for x being set st x in I holds
ex R being non empty multMagma st
( R = F . x & f . x in the carrier of R )