take
f
=
seq_const
0
;
:: thesis:
(
f
is
NAT
-valued
&
f
is
INT
-valued
)
thus
(
f
is
NAT
-valued
&
f
is
INT
-valued
) ;
:: thesis:
verum