reconsider
f
=
<*>
NAT
as
FinSequence
of
NAT
;
A1
:
f
/^
(
len
f
)
=
{}
by
RFINSEQ:27
;
per
cases
(
n
=
0
or
n
>
0
)
;
suppose
n
=
0
;
:: thesis:
{}
/^
n
is
empty
hence
{}
/^
n
is
empty
by
A1
;
:: thesis:
verum
end;
suppose
n
>
0
;
:: thesis:
{}
/^
n
is
empty
then
n
>
len
{}
;
hence
{}
/^
n
is
empty
by
RFINSEQ:def 1
;
:: thesis:
verum
end;
end;