deffunc H₁( Nat) -> object = [(f . $1),(f . ($1 + 1))];
ex p being FinSequence st
( len p = (len f) -' 1 & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider p being FinSequence such that
A1: len p = (len f) -' 1 and
A2: for k being Nat st k in dom p holds
p . k = [(f . k),(f . (k + 1))] ;
for i being Nat st 1 <= i & i < len f holds
p . i = [(f . i),(f . (i + 1))]

proof

let i be Nat; :: thesis: ( 1 <= i & i < len f implies p . i = [(f . i),(f . (i + 1))] )
assume that
A3: 1 <= i and
A4: i < len f ; :: thesis: p . i = [(f . i),(f . (i + 1))]
i + 1 <= len f by A4, NAT_1:13;
then A5: (i + 1) - 1 <= (len f) - 1 by XREAL_1:9;
(len f) - 1 = (len f) -' 1 by A3, A4, XREAL_1:233, XXREAL_0:2;
then i in dom p by A1, A3, A5, FINSEQ_3:25;
hence p . i = [(f . i),(f . (i + 1))] by A2; :: thesis: verum

end;

hence ex b₁ being FinSequence st
( len b₁ = (len f) -' 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . i = [(f . i),(f . (i + 1))] ) ) by A1; :: thesis: verum