defpred S₁[ 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₁[m] by A1;
A3: for n being Nat st S₁[n] holds
n <= len g ;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[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);

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

per cases ( k > 0 or k <= 0 ) ;

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;

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

per cases ( len g > 0 or len g <= 0 ) ;

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

then 0 + 1 <= len g by NAT_1:13;
hence len (smid (g,1,k)) = (k -' 1) + 1 by A4, A6, A7, FINSEQ_6:118
.= (k - 1) + 1 by A6, XREAL_1:233
.= k ;
:: thesis: verum

end;

case len g <= 0 ; :: thesis: contradiction

hence contradiction by A4, A5; :: thesis: verum

end;

end;

end;

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

end;

case A8: k <= 0 ; :: thesis: len (smid (g,1,k)) = k

then smid (g,1,k) = {} by Th7;
hence len (smid (g,1,k)) = k by A8; :: thesis: verum

end;

end;

end;

hence ex b₁ being FinSequence of D st
( len b₁ <= len g & b₁ = smid (g,1,(len b₁)) & b₁ = smid (f,(((len f) -' (len b₁)) + 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₁ ) ) by A4; :: thesis: verum