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 ;
then len (Rev CR) = 0 by FINSEQ_5:def 3;
then Rev CR is_preposition_of Rev r by FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence r = addcr (r,CR) by Th27; :: thesis: verum

end;

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

then 0 < len r by A1, FINSEQ_8:def 12;
then 0 + 1 <= len r by NAT_1:13;
then A3: 1 <= len (Rev r) by FINSEQ_5:def 3;
A4: 0 + 1 <= len CR by A2, NAT_1:13;
then (len CR) - 1 >= 0 by XREAL_1:48;
then A5: (len CR) -' 1 = (len CR) - 1 by XREAL_0:def 2;
A6: len r >= len CR by A1, FINSEQ_8:def 12;
then (len r) + 1 > len CR by NAT_1:13;
then A7: ((len r) + 1) - (len CR) > 0 by XREAL_1:50;
then A8: ((len r) + 1) -' (len CR) = ((len r) + 1) - (len CR) by XREAL_0:def 2;
A9: (len r) - (len CR) >= 0 by A6, XREAL_1:48;
then A10: (len r) - (len CR) = (len r) -' (len CR) by XREAL_0:def 2;
then A11: ( len (r /^ ((len r) -' (len CR))) = (len r) -' ((len r) -' (len CR)) & (len r) - ((len r) -' (len CR)) = (len r) -' ((len r) -' (len CR)) ) by RFINSEQ:29, XREAL_0:def 2;
instr (1,r,CR) = ((len r) + 1) -' (len CR) by A1, A2, FINSEQ_8:def 12;
then CR is_preposition_of r /^ ((((len r) + 1) -' (len CR)) -' 1) by A7, A8, FINSEQ_8:def 10;
then 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 A4, FINSEQ_6:def 3;
then A12: ((r /^ ((((len r) + 1) -' (len CR)) -' 1)) /^ 0) | (((len CR) -' 1) + 1) = CR by NAT_2:8;
(len r) - ((len r) -' (len CR)) >= 0 by NAT_D:35, XREAL_1:48;
then A13: (len r) -' ((len r) -' (len CR)) = (len r) - ((len r) -' (len CR)) by XREAL_0:def 2
.= (len r) - ((len r) - (len CR)) by A9, XREAL_0:def 2
.= len CR ;
((len r) + 1) - (len CR) >= 0 + 1 by A7, A8, NAT_1:13;
then (((len r) + 1) -' (len CR)) - 1 >= 0 by A8, XREAL_1:48;
then (((len r) + 1) -' (len CR)) -' 1 = (len r) - (len CR) by A8, XREAL_0:def 2;
then A14: (r /^ ((len r) -' (len CR))) | (len CR) = CR by A5, A10, A12;
mid ((Rev r),1,(len CR)) = ((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1) by A4, FINSEQ_6:def 3
.= ((Rev r) /^ 0) | (len CR) by A5, NAT_2:8
.= (Rev r) | ((len r) -' ((len r) -' (len CR))) by A13
.= Rev (r /^ ((len r) -' (len CR))) by Th18, NAT_D:35
.= Rev CR by A10, A14, A11, FINSEQ_1:58 ;
then mid ((Rev r),1,(len (Rev CR))) = Rev CR by FINSEQ_5:def 3;
then Rev CR is_preposition_of Rev r by A3, FINSEQ_8:def 8;
then CR is_postposition_of r by FINSEQ_8:def 9;
hence r = addcr (r,CR) by Th27; :: thesis: verum

end;

end;