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 A1: ( r1 is_terminated_by CR & r2 is_terminated_by CR & 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 A2: ( len r1 <= 0 & len r2 <= 0 ) ; :: thesis: ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR )

then A3: addcr f,CR is_preposition_of by FINSEQ_8:def 8;
addcr f,CR is_preposition_of by A2, FINSEQ_8:def 8;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A3, Def1; :: 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: len r1 = 0 by NAT_1:2;
A6: addcr f,CR is_preposition_of by A4, FINSEQ_8:def 8;
A7: f = r2 by A1, A5, Th3;
then addcr f,CR is_preposition_of by A1, Th29;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A6, A7, Def1; :: thesis: verum

end;

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

then A9: 0 + 1 <= len r1 by NAT_1:13;
0 <= len r2 by NAT_1:2;
then 1 + 0 <= (len r1) + (len r2) by A9, XREAL_1:9;
then A10: 1 <= len f by A1, FINSEQ_1:35;
A11: len f <= len (addcr f,CR) by Th31;
mid (addcr f,CR),1,(len r1) = (addcr f,CR) | (len r1) by A9, JORDAN3:25
.= (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 A1, FINSEQ_1:45
.= r1 | (len r1) by FINSEQ_5:25
.= r1 by FINSEQ_1:79 ;
then ( len r1 > 0 implies ( 1 <= len (addcr f,CR) & mid (addcr f,CR),1,(len r1) = r1 ) ) by A10, A11, XXREAL_0:2;
then A12: addcr f,CR is_preposition_of by FINSEQ_8:def 8;
addcr f,CR is_preposition_of by A8, FINSEQ_8:def 8;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A12, Def1; :: thesis: verum

end;

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

then A13: 0 + 1 <= len r1 by NAT_1:13;
0 <= len r2 by NAT_1:2;
then 1 + 0 <= (len r1) + (len r2) by A13, XREAL_1:9;
then A14: 1 <= len f by A1, FINSEQ_1:35;
A15: len f <= len (addcr f,CR) by Th31;
mid (addcr f,CR),1,(len r1) = (addcr f,CR) | (len r1) by A13, JORDAN3:25
.= (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 A1, FINSEQ_1:45
.= r1 | (len r1) by FINSEQ_5:25
.= r1 by FINSEQ_1:79 ;
then ( len r1 > 0 implies ( 1 <= len (addcr f,CR) & mid (addcr f,CR),1,(len r1) = r1 ) ) by A14, A15, XXREAL_0:2;
then A16: addcr f,CR is_preposition_of by FINSEQ_8:def 8;
CR ^ r2 is_substring_of addcr (r1 ^ r2),CR,1 by A1, Th37;
hence ( r1 is_a_record_of f,CR & r2 is_a_record_of f,CR ) by A1, A16, Def1; :: thesis: verum

end;

end;