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