let
k
be
Nat
;
:: thesis:
for
p
being
FinSequence
st not
k
in
dom
p
&
k
+
1
in
dom
p
holds
k
=
0
let
p
be
FinSequence
;
:: thesis:
( not
k
in
dom
p
&
k
+
1
in
dom
p
implies
k
=
0
)
assume
that
A1
: not
k
in
dom
p
and
A2
:
k
+
1
in
dom
p
;
:: thesis:
k
=
0
A3
:
k
+
1
<=
len
p
by
A2
,
FINSEQ_3:25
;
per
cases
(
k
<
1 or
k
>
len
p
)
by
A1
,
FINSEQ_3:25
;
suppose
k
<
1 ;
:: thesis:
k
=
0
hence
k
=
0
by
NAT_1:14
;
:: thesis:
verum
end;
suppose
k
>
len
p
;
:: thesis:
k
=
0
hence
k
=
0
by
A3
,
NAT_1:13
;
:: thesis:
verum
end;
end;