environ
vocabularies HIDDEN, XBOOLE_0, TREES_3, SUBSET_1, FINSET_1, TREES_2, TREES_1, CARD_1, ARYTM_3, NAT_1, ORDINAL4, FINSEQ_1, ARYTM_1, RELAT_1, FUNCT_1, TARSKI, ORDINAL1, NUMBERS, XXREAL_0, ZFMISC_1, TREES_4, FUNCT_6, TREES_A, TREES_9, MCART_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, NAT_1, BINOP_1, FINSET_1, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, TREES_3, TREES_4, MCART_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUNCT_1, TREES_2, TREES_3;
theorems TARSKI, AXIOMS, ZFMISC_1, NAT_1, WELLORD2, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, CARD_1, CARD_2, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, RELSET_1, RELAT_1, XBOOLE_0, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, FINSEQ_2, TREES_A, MCART_1, FINSEQ_6, XTUPLE_0;
schemes NAT_1, FUNCT_1, FINSEQ_1, CLASSES1, FUNCT_2, TREES_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, FINSEQ_1, TREES_1, TREES_2, TREES_3, PRE_CIRC, CARD_1, RELSET_1, NAT_1, XTUPLE_0;
constructors HIDDEN, WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, TREES_4, RELSET_1, BINOP_1, FINSEQ_4, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities TREES_2, TREES_4, BINOP_1, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, TREES_4;
Lm1:
for n being set
for p being FinSequence st n in dom p holds
ex k being Nat st
( n = k + 1 & k < len p )
Lm3:
for n being Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
scheme
FinOrdSet{
F1(
object )
-> set ,
F2()
-> finite set } :
for
n being
Nat holds
(
F1(
n)
in F2() iff
n < card F2() )
provided
A1:
for
x being
set st
x in F2() holds
ex
n being
Nat st
x = F1(
n)
and A2:
for
i,
j being
Nat st
i < j &
F1(
j)
in F2() holds
F1(
i)
in F2()
and A3:
for
i,
j being
Nat st
F1(
i)
= F1(
j) holds
i = j