n
<
n
+
1
by
NAT_1:13
;
then
A1
: (
X
.
(
n
+
1
)
=
{}
or
X
.
n
<>
{}
)
by
Def2
;
(
FuncsSeq
X
)
.
n
=
Funcs
(
(
X
.
(
n
+
1
)
)
,
(
X
.
n
)
)
by
Def3
;
hence
not
(
FuncsSeq
X
)
.
n
is
empty
by
A1
,
FUNCT_2:8
;
:: thesis:
verum