hereby :: thesis: ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b1 being FinSequence st b1 = {} )
deffunc H1( Nat) -> set = p . (m + (\$1 - 1));
assume that
1 <= m and
A1: m <= n and
n <= len p ; :: thesis: ex s being FinSequence st
( (len s) + m = n + 1 & ( for k being Nat st k < len s holds
s . (k + 1) = p . (m + k) ) )

consider s being FinSequence such that
A2: ( len s = (n + 1) -' m & ( for k being Nat st k in dom s holds
s . k = H1(k) ) ) from take s = s; :: thesis: ( (len s) + m = n + 1 & ( for k being Nat st k < len s holds
s . (k + 1) = p . (m + k) ) )

n <= n + 1 by XREAL_1:29;
then m <= n + 1 by ;
then m - m <= (n + 1) - m by XREAL_1:9;
then (len s) + m = ((n + 1) - m) + m by ;
hence (len s) + m = n + 1 ; :: thesis: for k being Nat st k < len s holds
s . (k + 1) = p . (m + k)

let k be Nat; :: thesis: ( k < len s implies s . (k + 1) = p . (m + k) )
assume k < len s ; :: thesis: s . (k + 1) = p . (m + k)
then A3: k + 1 <= len s by NAT_1:13;
0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom s by ;
hence s . (k + 1) = p . (m + ((k + 1) - 1)) by A2
.= p . (m + k) ;
:: thesis: verum
end;
thus ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b1 being FinSequence st b1 = {} ) ; :: thesis: verum