per
cases
(
x
in
dom
f
or not
x
in
dom
f
)
;
suppose
x
in
dom
f
;
:: thesis:
f
.
x
is
natural-valued
then
f
.
x
in
rng
f
by
FUNCT_1:def 3
;
hence
f
.
x
is
natural-valued
;
:: thesis:
verum
end;
suppose
not
x
in
dom
f
;
:: thesis:
f
.
x
is
natural-valued
hence
f
.
x
is
natural-valued
by
FUNCT_1:def 2
;
:: thesis:
verum
end;
end;