hereby :: thesis: ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b₁ being FinSequence st b₁ = {} )

deffunc H₁( 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 = H₁(k) ) ) from FINSEQ_1:sch 2();
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 A1, XXREAL_0:2;
then m - m <= (n + 1) - m by XREAL_1:9;
then (len s) + m = ((n + 1) - m) + m by A2, XREAL_0:def 2;
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 A3, FINSEQ_3:25;
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 b₁ being FinSequence st b₁ = {} ) ; :: thesis: verum