let D be non empty set ; 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; ( 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
; ( 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 A7:
(
len r1 > 0 &
len r2 <= 0 )
;
( 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;
verum end; suppose A11:
(
len r1 > 0 &
len r2 > 0 )
;
( 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;
verum end; end;