let D be non empty set ; :: thesis: for CR, r being File of D st r is_terminated_by CR holds
r = addcr r,CR
let CR, r be File of D; :: thesis: ( r is_terminated_by CR implies r = addcr r,CR )
assume A1: r is_terminated_by CR ; :: thesis: r = addcr r,CR

per cases ( len CR <= 0 or len CR > 0 ) ;

suppose len CR <= 0 ; :: thesis: r = addcr r,CR

then len CR = 0 by NAT_1:2;
then len (Rev CR) = 0 by FINSEQ_5:def 3;
then Rev r is_preposition_of by FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence r = addcr r,CR by Th28; :: thesis: verum

end;

suppose A2: len CR > 0 ; :: thesis: r = addcr r,CR

then A3: 0 + 1 <= len CR by NAT_1:13;
then (len CR) - 1 >= 0 by XREAL_1:50;
then A4: (len CR) -' 1 = (len CR) - 1 by XREAL_0:def 2;
A5: len r >= len CR by A1, A2, FINSEQ_8:def 12;
A6: 0 < len r by A1, A2, FINSEQ_8:def 12;
A7: (len r) - (len CR) >= 0 by A5, XREAL_1:50;
then A8: (len r) - (len CR) = (len r) -' (len CR) by XREAL_0:def 2;
(len r) + 1 > len CR by A5, NAT_1:13;
then A9: ((len r) + 1) - (len CR) > 0 by XREAL_1:52;
then A10: ((len r) + 1) -' (len CR) = ((len r) + 1) - (len CR) by XREAL_0:def 2;
then ((len r) + 1) - (len CR) >= 0 + 1 by A9, NAT_1:13;
then (((len r) + 1) -' (len CR)) - 1 >= 0 by A10, XREAL_1:50;
then A11: (((len r) + 1) -' (len CR)) -' 1 = (len r) - (len CR) by A10, XREAL_0:def 2;
instr 1,r,CR = ((len r) + 1) -' (len CR) by A1, A2, FINSEQ_8:def 12;
then r /^ ((((len r) + 1) -' (len CR)) -' 1) is_preposition_of by A9, A10, FINSEQ_8:def 10;
then ( 1 <= len (r /^ ((((len r) + 1) -' (len CR)) -' 1)) & mid (r /^ ((((len r) + 1) -' (len CR)) -' 1)),1,(len CR) = CR ) by A2, FINSEQ_8:def 8;
then ((r /^ ((((len r) + 1) -' (len CR)) -' 1)) /^ (1 -' 1)) | (((len CR) -' 1) + 1) = CR by A3, JORDAN3:def 1;
then ((r /^ ((((len r) + 1) -' (len CR)) -' 1)) /^ 0 ) | (((len CR) -' 1) + 1) = CR by NAT_2:10;
then A12: (r /^ ((len r) -' (len CR))) | (len CR) = CR by A4, A8, A11, FINSEQ_5:31;
A13: len (r /^ ((len r) -' (len CR))) = (len r) -' ((len r) -' (len CR)) by JORDAN3:19;
A14: (len r) - ((len r) -' (len CR)) = (len r) -' ((len r) -' (len CR)) by A2, A8, XREAL_0:def 2;
(len r) - ((len r) -' (len CR)) >= 0 by NAT_D:35, XREAL_1:50;
then A15: (len r) -' ((len r) -' (len CR)) = (len r) - ((len r) -' (len CR)) by XREAL_0:def 2
.= (len r) - ((len r) - (len CR)) by A7, XREAL_0:def 2
.= len CR ;
A16: mid (Rev r),1,(len CR) = ((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1) by A3, JORDAN3:def 1
.= ((Rev r) /^ 0 ) | (len CR) by A4, NAT_2:10
.= (Rev r) | ((len r) -' ((len r) -' (len CR))) by A15, FINSEQ_5:31
.= Rev (r /^ ((len r) -' (len CR))) by Th18, NAT_D:35
.= Rev CR by A8, A12, A13, A14, FINSEQ_1:79 ;
0 + 1 <= len r by A6, NAT_1:13;
then ( len (Rev CR) > 0 & 1 <= len (Rev r) & mid (Rev r),1,(len (Rev CR)) = Rev CR ) by A2, A16, FINSEQ_5:def 3;
then Rev r is_preposition_of by FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence r = addcr r,CR by Th28; :: thesis: verum

end;

end;