deffunc H_{1}( Nat) -> Element of the carrier of L = p . (n + $1);

consider ps being AlgSequence of L such that

A1: len ps <= len p and

A2: for k being Nat st k < len p holds

ps . k = H_{1}(k)
from ALGSEQ_1:sch 1();

take ps ; :: thesis: for i being Nat holds ps . i = p . (n + i)

let i be Nat; :: thesis: ps . i = p . (n + i)

consider ps being AlgSequence of L such that

A1: len ps <= len p and

A2: for k being Nat st k < len p holds

ps . k = H

take ps ; :: thesis: for i being Nat holds ps . i = p . (n + i)

let i be Nat; :: thesis: ps . i = p . (n + i)