per
cases
(
x
in
dom
f
or not
x
in
dom
f
)
;
suppose
A1
:
x
in
dom
f
;
:: thesis:
f
.
x
is
finite
Subset
of
NAT
A2
:
rng
f
c=
bool
NAT
by
Def2
;
f
.
x
in
rng
f
by
A1
,
FUNCT_1:3
;
hence
f
.
x
is
finite
Subset
of
NAT
by
A2
;
:: thesis:
verum
end;
suppose
not
x
in
dom
f
;
:: thesis:
f
.
x
is
finite
Subset
of
NAT
then
f
.
x
=
{}
by
FUNCT_1:def 2
;
hence
f
.
x
is
finite
Subset
of
NAT
by
XBOOLE_1:2
;
:: thesis:
verum
end;
end;