let D be non empty set ; :: thesis: for CR, r1, r2, f being File of D st r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 holds
( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )
let CR, r1, r2, f be File of D; :: thesis: ( r1 is_terminated_by CR & r2 is_terminated_by CR & f = r1 ^ r2 implies ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) )
assume that
A1: r1 is_terminated_by CR and
A2: r2 is_terminated_by CR and
A3: f = r1 ^ r2 ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

per cases ( ( len r1 <= 0 & len r2 <= 0 ) or ( len r1 <= 0 & len r2 > 0 ) or ( len r1 > 0 & len r2 <= 0 ) or ( len r1 > 0 & len r2 > 0 ) ) ;

suppose ( len r1 <= 0 & len r2 <= 0 ) ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

then ( r1 is_preposition_of addcr (f,CR) & r2 is_preposition_of addcr (f,CR) ) by FINSEQ_8:def 8;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2; :: thesis: verum

end;

suppose A4: ( len r1 <= 0 & len r2 > 0 ) ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

then A5: r1 is_preposition_of addcr (f,CR) by FINSEQ_8:def 8;
len r1 = 0 by A4;
then A6: f = r2 by A3, Th3;
then f is_preposition_of addcr (f,CR) by A2, Th28;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A5, A6; :: thesis: verum

end;

suppose A7: ( len r1 > 0 & len r2 <= 0 ) ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

1 + 0 <= (len r1) + (len r2) by A7, NAT_1:13;
then A8: 1 <= len f by A3, FINSEQ_1:22;
0 + 1 <= len r1 by A7, NAT_1:13;
then A9: mid ((addcr (f,CR)),1,(len r1)) = (addcr (f,CR)) | (len r1) by FINSEQ_6:116
.= (ovlcon (f,CR)) | (len r1) by FINSEQ_8:def 11
.= (f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) by FINSEQ_8:def 3
.= (r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) by A3, FINSEQ_1:32
.= r1 | (len r1) by FINSEQ_5:22
.= r1 by FINSEQ_1:58 ;
len f <= len (addcr (f,CR)) by Th30;
then ( len r1 > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len r1)) = r1 ) ) by A8, A9, XXREAL_0:2;
then A10: r1 is_preposition_of addcr (f,CR) by FINSEQ_8:def 8;
r2 is_preposition_of addcr (f,CR) by A7, FINSEQ_8:def 8;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A10; :: thesis: verum

end;

suppose A11: ( len r1 > 0 & len r2 > 0 ) ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

then 1 + 0 <= (len r1) + (len r2) by NAT_1:13;
then A12: 1 <= len f by A3, FINSEQ_1:22;
0 + 1 <= len r1 by A11, NAT_1:13;
then A13: mid ((addcr (f,CR)),1,(len r1)) = (addcr (f,CR)) | (len r1) by FINSEQ_6:116
.= (ovlcon (f,CR)) | (len r1) by FINSEQ_8:def 11
.= (f ^ (CR /^ (len (ovlpart (f,CR))))) | (len r1) by FINSEQ_8:def 3
.= (r1 ^ (r2 ^ (CR /^ (len (ovlpart (f,CR)))))) | (len r1) by A3, FINSEQ_1:32
.= r1 | (len r1) by FINSEQ_5:22
.= r1 by FINSEQ_1:58 ;
len f <= len (addcr (f,CR)) by Th30;
then ( len r1 > 0 implies ( 1 <= len (addcr (f,CR)) & mid ((addcr (f,CR)),1,(len r1)) = r1 ) ) by A12, A13, XXREAL_0:2;
then A14: r1 is_preposition_of addcr (f,CR) by FINSEQ_8:def 8;
CR ^ r2 is_substring_of addcr ((r1 ^ r2),CR),1 by A1, A2, Th36;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A2, A3, A14; :: thesis: verum

end;

end;