reconsider
mk
=
mk
as
Element
of
NAT
by
ORDINAL1:def 12
;
take
mk
;
:: thesis:
ex
f
being
FinSequence
of
NAT
st
(
f
=
x
`2_3
&
mk
=
f
/.
1 )
take
<*
mk
*>
;
:: thesis:
(
<*
mk
*>
=
x
`2_3
&
mk
=
<*
mk
*>
/.
1 )
thus
(
<*
mk
*>
=
x
`2_3
&
mk
=
<*
mk
*>
/.
1 )
by
A1
,
FINSEQ_4:16
;
:: thesis:
verum