consider
X
being non
empty
set
such that
A1
:
S
c=
[:
NAT
,
(
NAT
*
)
,
(
X
*
)
:]
by
Def1
;
I
=
[
(
I
`1_3
)
,
(
I
`2_3
)
,
(
I
`3_3
)
]
by
A1
,
RECDEF_2:3
;
then
[
(
I
`1_3
)
,
(
I
`2_3
)
]
in
proj1
S
by
XTUPLE_0:def 12
;
hence
InsCode
I
is
InsType
of
S
by
XTUPLE_0:def 12
;
:: thesis:
verum