defpred S_{1}[ Nat] means ( $1 <= len g & smid (g,1,$1) = smid (f,(((len f) -' $1) + 1),(len f)) );

A1: smid (g,1,0) = {} by Th7;

((len f) -' 0) + 1 = ((len f) - 0) + 1 by XREAL_1:233

.= (len f) + 1 ;

then smid (f,(((len f) -' 0) + 1),(len f)) = {} by Th7, XREAL_1:29;

then A2: ex m being Nat st S_{1}[m]
by A1;

A3: for n being Nat st S_{1}[n] holds

n <= len g ;

consider k being Nat such that

A4: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

n <= k ) ) from NAT_1:sch 6(A3, A2);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set b = smid (g,1,k);

_{1} being FinSequence of D st

( len b_{1} <= len g & b_{1} = smid (g,1,(len b_{1})) & b_{1} = smid (f,(((len f) -' (len b_{1})) + 1),(len f)) & ( for j being Nat st j <= len g & smid (g,1,j) = smid (f,(((len f) -' j) + 1),(len f)) holds

j <= len b_{1} ) )
by A4; :: thesis: verum

A1: smid (g,1,0) = {} by Th7;

((len f) -' 0) + 1 = ((len f) - 0) + 1 by XREAL_1:233

.= (len f) + 1 ;

then smid (f,(((len f) -' 0) + 1),(len f)) = {} by Th7, XREAL_1:29;

then A2: ex m being Nat st S

A3: for n being Nat st S

n <= len g ;

consider k being Nat such that

A4: ( S

n <= k ) ) from NAT_1:sch 6(A3, A2);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

set b = smid (g,1,k);

now :: thesis: ( ( k > 0 & len (smid (g,1,k)) = k ) or ( k <= 0 & len (smid (g,1,k)) = k ) )end;

hence
ex bper cases
( k > 0 or k <= 0 )
;

end;

case A5:
k > 0
; :: thesis: len (smid (g,1,k)) = k

then A6:
0 + 1 <= k
by NAT_1:13;

then A7: smid (g,1,k) = mid (g,1,k) by Th4;

end;then A7: smid (g,1,k) = mid (g,1,k) by Th4;

now :: thesis: ( ( len g > 0 & len (smid (g,1,k)) = k ) or ( len g <= 0 & contradiction ) )

hence
len (smid (g,1,k)) = k
; :: thesis: verumend;

( len b

j <= len b