environ
vocabularies HIDDEN, NUMBERS, TREES_1, SUBSET_1, FUNCT_1, XBOOLE_0, FINSEQ_1, ORDINAL4, XXREAL_0, ARYTM_3, RELAT_1, TARSKI, CARD_1, NAT_1, ORDINAL1, FINSET_1, REAL_1, ARYTM_1, ZFMISC_1, FUNCOP_1, TREES_2, AMISTD_3, FINSEQ_2, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, XCMPLX_0, FUNCT_1, PARTFUN1, XREAL_0, REAL_1, NAT_1, CARD_1, NUMBERS, FINSEQ_1, FINSEQ_2, FINSET_1, RELSET_1, BINOP_1, FUNCT_2, FUNCOP_1, TREES_1, XXREAL_0;
definitions RELAT_1, TARSKI, FUNCT_1, TREES_1, ORDINAL1, XBOOLE_0;
theorems FUNCT_1, NAT_1, FINSEQ_1, TREES_1, TARSKI, ORDERS_1, ZFMISC_1, FINSET_1, CARD_1, CARD_2, WELLORD2, FUNCOP_1, FUNCT_2, RELAT_1, FINSEQ_2, ORDINAL1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, RELSET_1, XTUPLE_0, XREAL_0;
schemes FUNCT_1, FRAENKEL, NAT_1, CARD_2, CLASSES1, DOMAIN_1, XBOOLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, TREES_1, CARD_1, FINSEQ_2, PARTFUN1;
constructors HIDDEN, WELLORD2, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, TREES_1, RELSET_1, FINSEQ_2, XREAL_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TREES_1, BINOP_1, CARD_1, ORDINAL1;
expansions RELAT_1, TARSKI, FUNCT_1, TREES_1, ORDINAL1, XBOOLE_0;
scheme
FuncExOfMinNat{
P1[
object ,
Nat],
F1()
-> set } :
ex
f being
Function st
(
dom f = F1() & ( for
x being
object st
x in F1() holds
ex
n being
Nat st
(
f . x = n &
P1[
x,
n] & ( for
m being
Nat st
P1[
x,
m] holds
n <= m ) ) ) )
provided
A1:
for
x being
object st
x in F1() holds
ex
n being
Nat st
P1[
x,
n]
Lm1:
for X being set st X is finite holds
ex n being Nat st
for k being Nat st k in X holds
k <= n