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

thus
( ( not 1 <= m or not m <= n or not n <= len p ) implies ex bdeffunc H_{1}( 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_{1}(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;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

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