thus
( n <= len f implies ex p1 being FinSequence st

( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) ) ) :: thesis: ( not n <= len f implies ex b_{1} being FinSequence st b_{1} = {} )_{1} being FinSequence st b_{1} = {} )
; :: thesis: verum

( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) ) ) :: thesis: ( not n <= len f implies ex b

proof

thus
( not n <= len f implies ex b
assume
n <= len f
; :: thesis: ex p1 being FinSequence st

( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) )

then reconsider k = (len f) - n as Element of NAT by NAT_1:21;

deffunc H_{1}( Nat) -> set = f . ($1 + n);

consider p being FinSequence such that

A1: ( len p = k & ( for m being Nat st m in dom p holds

p . m = H_{1}(m) ) )
from FINSEQ_1:sch 2();

take p ; :: thesis: ( len p = (len f) - n & ( for m being Nat st m in dom p holds

p . m = f . (m + n) ) )

thus len p = (len f) - n by A1; :: thesis: for m being Nat st m in dom p holds

p . m = f . (m + n)

let m be Nat; :: thesis: ( m in dom p implies p . m = f . (m + n) )

assume m in dom p ; :: thesis: p . m = f . (m + n)

hence p . m = f . (m + n) by A1; :: thesis: verum

end;( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) )

then reconsider k = (len f) - n as Element of NAT by NAT_1:21;

deffunc H

consider p being FinSequence such that

A1: ( len p = k & ( for m being Nat st m in dom p holds

p . m = H

take p ; :: thesis: ( len p = (len f) - n & ( for m being Nat st m in dom p holds

p . m = f . (m + n) ) )

thus len p = (len f) - n by A1; :: thesis: for m being Nat st m in dom p holds

p . m = f . (m + n)

let m be Nat; :: thesis: ( m in dom p implies p . m = f . (m + n) )

assume m in dom p ; :: thesis: p . m = f . (m + n)

hence p . m = f . (m + n) by A1; :: thesis: verum