defpred S1[ 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 S1[m] by A1;
A3: for n being Nat st S1[n] holds
n <= len g ;
consider k being Nat such that
A4: ( S1[k] & ( for n being Nat st S1[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;
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 b1 being FinSequence of D st
( len b1 <= len g & b1 = smid (g,1,(len b1)) & b1 = smid (f,(((len f) -' (len b1)) + 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 b1 ) ) by A4; :: thesis: verum