environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0, FUNCOP_1, ORDINAL3, ORDINAL2, TARSKI, SUBSET_1, SETFAM_1, ZFMISC_1, MCART_1, FUNCT_4, FINSET_1, MATROID0, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, RELAT_1, FUNCT_1, FUNCOP_1, MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3, SUBSET_1, DOMAIN_1, RELSET_1, FUNCT_2, FUNCT_3, FUNCT_4;
definitions TARSKI, XBOOLE_0;
theorems FUNCT_1, ENUMSET1, ZFMISC_1, TARSKI, RELAT_1, ORDINAL3, ORDINAL1, XBOOLE_0, XBOOLE_1, FUNCT_3, FUNCOP_1, FUNCT_4, SUBSET_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, ORDINAL2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2, RELSET_1, FUNCOP_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, FUNCT_3, FUNCOP_1, ORDINAL3, FUNCT_4, SETFAM_1, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities TARSKI, XBOOLE_0, FUNCOP_1, RELAT_1, FUNCT_4, ORDINAL1;
expansions TARSKI, XBOOLE_0, ORDINAL1;
Lm1:
for x being object holds {x} is finite
Lm2:
for A, B being set st A is finite & B is finite holds
A \/ B is finite
registration
let x1,
x2,
x3,
x4,
x5,
x6 be
object ;
coherence
{x1,x2,x3,x4,x5,x6} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
object ;
coherence
{x1,x2,x3,x4,x5,x6,x7} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
object ;
coherence
{x1,x2,x3,x4,x5,x6,x7,x8} is finite
end;
scheme
Finite{
F1()
-> set ,
P1[
set ] } :
provided
A1:
F1() is
finite
and A2:
P1[
{} ]
and A3:
for
x,
B being
set st
x in F1() &
B c= F1() &
P1[
B] holds
P1[
B \/ {x}]
Lm3:
for A being set st A is finite & ( for X being set st X in A holds
X is finite ) holds
union A is finite
deffunc H1( object ) -> object = $1 `1 ;