deffunc
H
_{1}
(
Nat
)
->
Element
of
R
=
x
;
consider
p
being
AlgSequence
of
R
such that
A1
: (
len
p
<=
1 & ( for
k
being
Nat
st
k
<
1 holds
p
.
k
=
H
_{1}
(
k
) ) )
from
ALGSEQ_1:sch 1
();
take
p
;
:: thesis:
(
len
p
<=
1 &
p
.
0
=
x
)
thus
(
len
p
<=
1 &
p
.
0
=
x
)
by
A1
;
:: thesis:
verum