let D be non empty set ; :: thesis: for f, CR being File of D holds CR is_substring_of ovlcon f,CR,1
let f, CR be File of D; :: thesis: CR is_substring_of ovlcon f,CR,1

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

suppose A1: len CR > 0 ; :: thesis: CR is_substring_of ovlcon f,CR,1

set i3 = (len f) -' (len (ovlpart f,CR));
A2: len CR >= 0 + 1 by A1, NAT_1:13;
then A3: ((len f) -' (len (ovlpart f,CR))) + 1 <= ((len f) -' (len (ovlpart f,CR))) + (len CR) by XREAL_1:8;
then A4: ((((len f) -' (len (ovlpart f,CR))) + (len CR)) -' (((len f) -' (len (ovlpart f,CR))) + 1)) + 1 = ((((len f) -' (len (ovlpart f,CR))) + (len CR)) - (((len f) -' (len (ovlpart f,CR))) + 1)) + 1 by XREAL_1:235
.= len CR ;
1 - (len (ovlpart f,CR)) <= (len CR) - (len (ovlpart f,CR)) by A2, XREAL_1:11;
then (1 - (len (ovlpart f,CR))) + (len f) <= ((len CR) - (len (ovlpart f,CR))) + (len f) by XREAL_1:9;
then A5: ( (len f) - (len (ovlpart f,CR)) >= 0 & ((len f) - (len (ovlpart f,CR))) + 1 <= (len f) + ((len CR) - (len (ovlpart f,CR))) ) by FINSEQ_8:10, XREAL_1:50;
len (ovlpart f,CR) <= len CR by FINSEQ_8:def 2;
then A6: (len CR) - (len (ovlpart f,CR)) >= 0 by XREAL_1:50;
set i4 = ((len f) -' (len (ovlpart f,CR))) + 1;
A7: (len f) -' (len (ovlpart f,CR)) <= len (f | ((len f) -' (len (ovlpart f,CR)))) by FINSEQ_1:80, NAT_D:35;
A8: (f | ((len f) -' (len (ovlpart f,CR)))) /^ ((len f) -' (len (ovlpart f,CR))) = (f /^ ((len f) -' (len (ovlpart f,CR)))) | (((len f) -' (len (ovlpart f,CR))) -' ((len f) -' (len (ovlpart f,CR)))) by FINSEQ_5:83
.= (f /^ ((len f) -' (len (ovlpart f,CR)))) | 0 by XREAL_1:234
.= {} ;
len (CR /^ (len (ovlpart f,CR))) = (len CR) -' (len (ovlpart f,CR)) by RFINSEQ:42
.= (len CR) - (len (ovlpart f,CR)) by A6, XREAL_0:def 2 ;
then ( ovlcon f,CR = f ^ (CR /^ (len (ovlpart f,CR))) & ((len f) -' (len (ovlpart f,CR))) + 1 <= (len f) + (len (CR /^ (len (ovlpart f,CR)))) ) by A5, FINSEQ_8:def 3, XREAL_0:def 2;
then A9: ( 1 <= ((len f) -' (len (ovlpart f,CR))) + 1 & ((len f) -' (len (ovlpart f,CR))) + 1 <= len (ovlcon f,CR) ) by FINSEQ_1:35, NAT_1:11;
mid (ovlcon f,CR),(((len f) -' (len (ovlpart f,CR))) + 1),(((((len f) -' (len (ovlpart f,CR))) + 1) -' 1) + (len CR)) = mid ((f | ((len f) -' (len (ovlpart f,CR)))) ^ CR),(((len f) -' (len (ovlpart f,CR))) + 1),(((((len f) -' (len (ovlpart f,CR))) + 1) -' 1) + (len CR)) by FINSEQ_8:11
.= mid ((f | ((len f) -' (len (ovlpart f,CR)))) ^ CR),(((len f) -' (len (ovlpart f,CR))) + 1),(((len f) -' (len (ovlpart f,CR))) + (len CR)) by NAT_D:34
.= (((f | ((len f) -' (len (ovlpart f,CR)))) ^ CR) /^ ((((len f) -' (len (ovlpart f,CR))) + 1) -' 1)) | (((((len f) -' (len (ovlpart f,CR))) + (len CR)) -' (((len f) -' (len (ovlpart f,CR))) + 1)) + 1) by A3, FINSEQ_6:def 3
.= (((f | ((len f) -' (len (ovlpart f,CR)))) ^ CR) /^ ((len f) -' (len (ovlpart f,CR)))) | (len CR) by A4, NAT_D:34
.= (((f | ((len f) -' (len (ovlpart f,CR)))) /^ ((len f) -' (len (ovlpart f,CR)))) ^ CR) | (len CR) by A7, GENEALG1:1
.= CR | (len CR) by A8, FINSEQ_1:47
.= CR by Th2 ;
hence CR is_substring_of ovlcon f,CR,1 by A9, FINSEQ_8:def 7; :: thesis: verum

end;

suppose len CR <= 0 ; :: thesis: CR is_substring_of ovlcon f,CR,1

hence CR is_substring_of ovlcon f,CR,1 by FINSEQ_8:def 7; :: thesis: verum

end;

end;