deffunc H₁( 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₁(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)

per cases ( i < len p or i >= len p ) ;

suppose i < len p ; :: thesis: ps . i = p . (n + i)

hence ps . i = p . (n + i) by A2; :: thesis: verum

end;

suppose A3: i >= len p ; :: thesis: ps . i = p . (n + i)

hence ps . i = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2
.= p . (n + i) by A3, ALGSEQ_1:8, NAT_1:12 ;
:: thesis: verum

end;

end;