environ
vocabularies HIDDEN, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, XXREAL_0, GROUP_2, CARD_1, FUNCT_4, GROUP_6, GROUP_7, 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, ZFMISC_1, PBOOLE, NEWTON, INT_1, NAT_3, REAL_1, PRE_POLY, XCMPLX_0, UPROOTS, INT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, 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, BINOP_1, FINSEQ_1, NEWTON, PRE_POLY, NAT_3, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GROUP_7, INT_7;
definitions TARSKI, GROUP_2, FINSEQ_1, STRUCT_0;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, XREAL_0, FUNCOP_1, TARSKI, GROUP_1, GROUP_2, GROUP_3, EULER_1, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, ORDINAL1, FINSEQ_3, NAT_1, RFINSEQ, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7, STRUCT_0, PRVECT_3, CARD_2, INT_7, XBOOLE_1, NEWTON, PRE_POLY, GROUP_10, UPROOTS, PARTFUN1, NAT_3, INT_2, NAT_D, ZFMISC_1, GR_CY_1, CARD_1, WELLORD2, TOPALG_4;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, FUNCT_2, CARD_1, CARD_3, GROUP_7, GROUP_3, RELSET_1, FINSEQ_1, INT_1, AOFA_000, GR_CY_1, FINSET_1, NAT_3, RELAT_1, FUNCT_1, MEMBERED, FUNCOP_1, NEWTON, VALUED_0, PRE_POLY, PBOOLE, INT_7, GROUP_6, ORDINAL1;
constructors HIDDEN, BINOP_1, REALSET1, GROUP_6, MONOID_0, PRALG_1, GROUP_4, CARD_2, GROUP_7, RELSET_1, WELLORD2, NAT_D, INT_7, RECDEF_1, NAT_3, FINSOP_1;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities GROUP_2, FINSEQ_1, STRUCT_0, FUNCOP_1;
expansions STRUCT_0;
theorem Th1:
for
A,
B,
A1,
B1 being
set st
A misses B &
A1 c= A &
B1 c= B &
A1 \/ B1 = A \/ B holds
(
A1 = A &
B1 = B )
Lm1:
for ps, pt, f being bag of SetPrimes st ps is prime-factorization-like & pt is prime-factorization-like & f = ps + pt & support ps misses support pt holds
f is prime-factorization-like
Lm2:
for G being non empty multMagma
for I being non empty finite set
for b being b2 -defined the carrier of b1 -valued total Function holds
( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) )
Lm3:
for A, B being non empty finite set st A misses B holds
( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) )
Lm4:
for A, B being non empty finite set
for FA being b1 -defined total Function
for FB being b2 -defined total Function
for f, g being FinSequence
for FAB being b1 \/ b2 -defined Function st A misses B & FAB = FA +* FB & f = FA * (canFS A) & g = FB * (canFS B) holds
f ^ g = FAB * ((canFS A) ^ (canFS B))
Lm5:
for G being finite Group
for q being Prime st q in support (prime_factorization (card G)) holds
ex a being Element of G st
( a <> 1_ G & ord a = q )
Lm6:
for I being non empty set
for F being multMagma-Family of I
for x being set st x in the carrier of (product F) holds
x is b1 -defined total Function
Lm7:
for I being non empty set
for F being 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 )