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:235
.= (len f) + 1 ;
then smid f,(((len f) -' 0 ) + 1),(len f) = {} by Th7, XREAL_1:31;
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 13;
set b = smid g,1,k;

now

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

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, JORDAN3:27
.= (k - 1) + 1 by A6, XREAL_1:235
.= 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 A9: k = 0 ;
smid g,1,k = {} by A8, Th7;
hence len (smid g,1,k) = k by A9; :: 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