let D be non empty set ; :: thesis: for CR, r1, r2 being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR holds
CR ^ r2 is_substring_of addcr (r1 ^ r2),CR,1
let CR, r1, r2 be File of D; :: thesis: ( r1 is_terminated_by CR & r2 is_terminated_by CR implies CR ^ r2 is_substring_of addcr (r1 ^ r2),CR,1 )
assume A1: ( r1 is_terminated_by CR & r2 is_terminated_by CR ) ; :: thesis: CR ^ r2 is_substring_of addcr (r1 ^ r2),CR,1
then r1 = addcr r1,CR by Th29;
then A2: r1 = ovlcon r1,CR by FINSEQ_8:def 11;
r2 = addcr r2,CR by A1, Th29;
then r2 = ovlcon r2,CR by FINSEQ_8:def 11;
then r2 = r2 ^ (CR /^ (len (ovlpart r2,CR))) by FINSEQ_8:def 3;
then A3: r1 ^ r2 = ((r1 | ((len r1) -' (len (ovlpart r1,CR)))) ^ CR) ^ (r2 ^ (CR /^ (len (ovlpart r2,CR)))) by A2, FINSEQ_8:11;
addcr (r1 ^ r2),CR = ovlcon (r1 ^ r2),CR by FINSEQ_8:def 11
.= (r1 ^ r2) ^ (CR /^ (len (ovlpart (r1 ^ r2),CR))) by FINSEQ_8:def 3
.= (((r1 | ((len r1) -' (len (ovlpart r1,CR)))) ^ (CR ^ r2)) ^ (CR /^ (len (ovlpart r2,CR)))) ^ (CR /^ (len (ovlpart (r1 ^ r2),CR))) by A3, Th1
.= ((r1 | ((len r1) -' (len (ovlpart r1,CR)))) ^ (CR ^ r2)) ^ ((CR /^ (len (ovlpart r2,CR))) ^ (CR /^ (len (ovlpart (r1 ^ r2),CR)))) by FINSEQ_1:45 ;
hence CR ^ r2 is_substring_of addcr (r1 ^ r2),CR,1 by Th36; :: thesis: verum