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 b1 being FinSequence st b1 = {} )
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 H1( 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 = H1(m) ) ) from 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 b1 being FinSequence st b1 = {} ) ; :: thesis: verum