deffunc H_{1}( 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_{1}(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))]_{1} being FinSequence st

( len b_{1} = (len f) -' 1 & ( for i being Nat st 1 <= i & i < len f holds

b_{1} . i = [(f . i),(f . (i + 1))] ) )
by A1; :: thesis: verum

ex p being FinSequence st

( len p = (len f) -' 1 & ( for k being Nat st k in dom p holds

p . k = H

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

hence
ex b
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;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

( len b

b