begin
Lm1:
for x being set 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
set ;
coherence
{x1,x2,x3,x4,x5,x6} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
coherence
{x1,x2,x3,x4,x5,x6,x7} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
set ;
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
begin
deffunc H1( set ) -> set = $1 `1 ;