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