ex
f
being
sequence
of
(
product
(
the_Values_of
S
)
)
st
(
Comput
(
p
,
s
,
0
)
=
f
.
0
&
f
.
0
=
s
& ( for
i
being
Nat
holds
f
.
(
i
+
1
)
=
Following
(
p
,
(
f
.
i
)
) ) )
by
Def7
;
hence
Comput
(
p
,
s
,
0
)
=
s
;
:: thesis:
verum