let
f
be non
empty
XFinSequence
;
:: thesis:
f

1
=
<%
(
f
.
0
)
%>
A1
:
0
in
Segm
(
0
+
1
)
by
NAT_1:45
;
len
f
>=
1
by
NAT_1:14
;
then
(
len
(
f

1
)
=
1 &
(
f

1
)
.
0
=
f
.
0
)
by
AFINSQ_1:54
,
FUNCT_1:49
,
A1
;
hence
f

1
=
<%
(
f
.
0
)
%>
by
AFINSQ_1:34
;
:: thesis:
verum