environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0, BINOP_1, FUNCT_1, FINSOP_1, SETWISEO, XXREAL_0, TARSKI, NAT_1, ARYTM_3, WELLORD1, FINSUB_1, SETFAM_1, ORDERS_1, FINSET_1, ZFMISC_1, CARD_1, PARTFUN1, ARROW, ORDINAL2, ORDINAL1, RELAT_2, ARYTM_1, FINSEQ_3, FUNCOP_1, PBOOLE, FUNCT_4, FINSEQ_2, CARD_3, MEMBER_1, VALUED_0, FUNCT_2, BINOP_2, CLASSES1, PRE_POLY, FINSEQ_5, XCMPLX_0, WELLORD2, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, WELLORD2, RELAT_1, XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, FINSET_1, FINSUB_1, SETWISEO, PARTFUN1, FUNCT_2, BINOP_2, FINSOP_1, FINSEQ_1, FINSEQ_4, FUNCT_3, BINOP_1, XREAL_0, FINSEQ_2, FUNCT_4, FINSEQ_5, WELLORD1, ORDERS_1, CARD_3, WSIERP_1, FUNCOP_1, FUNCT_7, NAT_D, INT_1, NAT_1, CLASSES1, VALUED_0, VALUED_1, ORDINAL2, SETFAM_1, DOMAIN_1, ARROW, FINSEQOP;
definitions TARSKI, XBOOLE_0, CARD_3, RELAT_2, WELLORD2, RELAT_1, VALUED_0, FUNCOP_1, SETFAM_1, FUNCT_1;
theorems FUNCT_1, FINSET_1, FINSEQ_3, FINSEQ_4, ZFMISC_1, FINSEQ_1, FUNCT_2, FUNCOP_1, TARSKI, FUNCT_7, BINOP_1, RELAT_1, FINSEQ_2, CARD_3, RFINSEQ, RELSET_1, CARD_1, ORDINAL1, RVSUM_1, FINSEQ_5, NAT_1, PBOOLE, NAT_2, SUBSET_1, ORDERS_1, WELLSET1, RELAT_2, ORDINAL3, FINSEQ_6, SETWISEO, SETWOP_2, CARD_2, FUNCT_5, FINSUB_1, PARTFUN2, XBOOLE_0, XBOOLE_1, PARTFUN1, BINOP_2, XREAL_1, XXREAL_0, VALUED_0, VALUED_1, NAT_D, SETFAM_1, ARROW, WELLORD2, FINSOP_1, INT_1, XTUPLE_0, FUNCT_4;
schemes SETWISEO, FUNCT_2, FINSEQ_2, FINSEQ_1, PBOOLE, RELSET_1, FINSEQ_4, ORDINAL1, FUNCT_7, SUBSET_1, XBOOLE_0, BINOP_1, NAT_1, PRE_CIRC, CLASSES1, INT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL3, FINSET_1, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, FINSEQ_2, CARD_3, PARTFUN1, VALUED_0, VALUED_1, RELSET_1, FUNCT_2, SETFAM_1, FINSUB_1, INT_1, PBOOLE;
constructors HIDDEN, WELLORD2, BINOP_1, SETWISEO, CARD_3, FINSEQOP, FINSOP_1, FINSEQ_4, RFINSEQ, RFUNCT_3, NAT_D, WSIERP_1, FUNCT_7, RECDEF_1, BINOP_2, CLASSES1, BINARITH, ARROW, TOLER_1, ORDINAL2, RELSET_1, ORDERS_1, RELAT_2, WELLORD1, DOMAIN_1, SETFAM_1, ORDINAL3, PBOOLE, FINSEQ_5, REAL_1, FUNCT_4, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities PBOOLE, BINOP_1, FINSEQ_2, FUNCOP_1, WELLORD1, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, CARD_3, RELAT_2, PBOOLE, RELAT_1, BINOP_1, VALUED_0, WELLORD1, FUNCT_1;
scheme
Regr1{
F1()
-> Nat,
P1[
set ] } :
provided
A1:
P1[
F1()]
and A2:
for
k being
Element of
NAT st
k < F1() &
P1[
k + 1] holds
P1[
k]
theorem Th40:
for
n being
Ordinal for
p,
q,
r being
bag of
n st
p < q &
q < r holds
p < r
theorem Th46:
for
n being
set for
b1,
b2 being
bag of
n st
b1 divides b2 holds
(b2 -' b1) + b1 = b2
theorem Th47:
for
X being
set for
b1,
b2 being
bag of
X holds
(b2 + b1) -' b1 = b2
theorem Th49:
for
n being
set for
b,
b1,
b2 being
bag of
n st
b = b1 + b2 holds
b1 divides b
Lm1:
for n being Ordinal holds BagOrder n is_reflexive_in Bags n
by Def13;
Lm2:
for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n
Lm3:
for n being Ordinal holds BagOrder n is_transitive_in Bags n
Lm4:
for n being Ordinal holds BagOrder n linearly_orders Bags n
Lm5:
for D being set
for p being FinSequence of D st dom p <> {} holds
1 in dom p
Lm6:
for X being set
for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
Lm7:
for X being set
for b being bag of X holds b is PartFunc of X,NAT
Lm8:
for X being set
for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )