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 len CR > 0 ; :: thesis: CR is_substring_of ovlcon f,CR,1

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