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:6;
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:233
.= len CR ;
1 - (len (ovlpart (f,CR))) <= (len CR) - (len (ovlpart (f,CR))) by A2, XREAL_1:9;
then (1 - (len (ovlpart (f,CR)))) + (len f) <= ((len CR) - (len (ovlpart (f,CR)))) + (len f) by XREAL_1:7;
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:48;
len (ovlpart (f,CR)) <= len CR by FINSEQ_8:def 2;
then A6: (len CR) - (len (ovlpart (f,CR))) >= 0 by XREAL_1:48;
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:59, 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:80
.= (f /^ ((len f) -' (len (ovlpart (f,CR))))) | 0 by XREAL_1:232
.= {} ;
len (CR /^ (len (ovlpart (f,CR)))) = (len CR) -' (len (ovlpart (f,CR))) by RFINSEQ:29
.= (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:22, 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:34
.= 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;