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 that
A1: r1 is_terminated_by CR and
A2: r2 is_terminated_by CR ; :: thesis: CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1
r2 = addcr (r2,CR) by A2, Th28;
then r2 = ovlcon (r2,CR) by FINSEQ_8:def 11;
then A3: r2 = r2 ^ (CR /^ (len (ovlpart (r2,CR)))) by FINSEQ_8:def 3;
r1 = addcr (r1,CR) by A1, Th28;
then r1 = ovlcon (r1,CR) by FINSEQ_8:def 11;
then A4: r1 ^ r2 = ((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ CR) ^ (r2 ^ (CR /^ (len (ovlpart (r2,CR))))) by A3, 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 A4, Th1
.= ((r1 | ((len r1) -' (len (ovlpart (r1,CR))))) ^ (CR ^ r2)) ^ ((CR /^ (len (ovlpart (r2,CR)))) ^ (CR /^ (len (ovlpart ((r1 ^ r2),CR))))) by FINSEQ_1:32 ;
hence CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 by Th35; :: thesis: verum