let
f
be
FinSequence
;
:: thesis:
for
i
being
Nat
st
i
>=
len
f
holds
f
/^
i
=
{}
let
i
be
Nat
;
:: thesis:
(
i
>=
len
f
implies
f
/^
i
=
{}
)
assume
A1
:
i
>=
len
f
;
:: thesis:
f
/^
i
=
{}
per
cases
(
i
>
len
f
or
i
=
len
f
)
by
A1
,
XXREAL_0:1
;
suppose
i
>
len
f
;
:: thesis:
f
/^
i
=
{}
hence
f
/^
i
=
{}
by
RFINSEQ:def 1
;
:: thesis:
verum
end;
suppose
A2
:
i
=
len
f
;
:: thesis:
f
/^
i
=
{}
then
len
(
f
/^
i
)
=
(
len
f
)

i
by
RFINSEQ:def 1
.=
0
by
A2
;
hence
f
/^
i
=
{}
;
:: thesis:
verum
end;
end;