per
cases
(
n
>
0
or
n
=
0
)
;
suppose
A1
:
n
>
0
;
:: thesis:
(
f

n
)
/^
n
is
empty
(
len
(
f

n
)
=
n
or not
n
in
dom
f
)
by
Th10
;
then
(
len
(
f

n
)
=
n
or
n
<
1 or
n
>
len
f
)
by
FINSEQ_3:25
;
then
len
(
f

n
)
<=
n
by
FINSEQ_1:58
,
A1
,
NAT_1:14
;
hence
(
f

n
)
/^
n
is
empty
by
FINSEQ_5:32
;
:: thesis:
verum
end;
suppose
n
=
0
;
:: thesis:
(
f

n
)
/^
n
is
empty
then
f

n
=
{}
;
hence
(
f

n
)
/^
n
is
empty
;
:: thesis:
verum
end;
end;