consider
X
being non
empty
set
such that
A1
:
S
c=
[:
NAT
,
(
NAT
*
)
,
(
X
*
)
:]
by
Def1
;
x
in
S
;
then
x
`1_3
in
NAT
by
A1
,
RECDEF_2:2
;
hence
InsCode
x
is
natural
;
:: thesis:
verum