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₁ being FinSequence st b₁ = {} )

proof

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₁( 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₁(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;

thus ( not n <= len f implies ex b₁ being FinSequence st b₁ = {} ) ; :: thesis: verum