let
p
be
FinSequence
;
:: thesis:
for
k
being
set
st
k
in
dom
p
holds
len
p
>
0
let
k
be
set
;
:: thesis:
(
k
in
dom
p
implies
len
p
>
0
)
assume
k
in
dom
p
;
:: thesis:
len
p
>
0
then
p
<>
{}
;
hence
len
p
>
0
;
:: thesis:
verum