A1
:
dom
(
NAT
-->
0
)
=
NAT
;
per
cases
(
k
in
NAT
or not
k
in
NAT
)
;
suppose
k
in
NAT
;
:: thesis:
(
NAT
-->
0
)
.
k
=
0
hence
(
NAT
-->
0
)
.
k
=
0
by
FUNCOP_1:7
;
:: thesis:
verum
end;
suppose
not
k
in
NAT
;
:: thesis:
(
NAT
-->
0
)
.
k
=
0
hence
(
NAT
-->
0
)
.
k
=
0
by
A1
,
FUNCT_1:def 2
;
:: thesis:
verum
end;
end;