let D be non empty set ; :: thesis: for CR, r being File of D st CR is_postposition_of r holds
r = addcr r,CR
let CR, r be File of D; :: thesis: ( CR is_postposition_of r implies r = addcr r,CR )
assume A1: CR is_postposition_of r ; :: thesis: r = addcr r,CR
A2: len CR = len (Rev CR) by FINSEQ_5:def 3;
A3: len r = len (Rev r) by FINSEQ_5:def 3;
0 <= (len r) - (len CR) by A1, Th27;
then A4: 0 + (len CR) <= ((len r) - (len CR)) + (len CR) by XREAL_1:9;
A5: Rev r is_preposition_of by A1, FINSEQ_8:def 9;

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

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

then A7: ( len CR <= len r & mid r,(((len r) + 1) -' (len CR)),(len r) = CR ) by A1, FINSEQ_8:24;
A8: len CR >= 0 + 1 by A6, NAT_1:13;
A9: len (Rev r) = ((len (Rev r)) - (len CR)) + (len CR) ;
Rev (mid (Rev r),1,(len CR)) = Rev (Rev CR) by A2, A5, A6, FINSEQ_8:def 8;
then A10: mid (Rev r),(len CR),1 = Rev (Rev CR) by JORDAN4:30
.= CR by FINSEQ_6:29 ;

now

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

case A11: len CR > 1 ; :: thesis: r = addcr r,CR

then len CR >= 1 + 1 by NAT_1:13;
then (len CR) - 1 >= (1 + 1) - 1 by XREAL_1:11;
then A12: ((len CR) -' 1) + 1 = len CR by NAT_D:43;
A13: (len (Rev r)) -' (len CR) = (len (Rev r)) - (len CR) by A3, A4, XREAL_1:235;
mid (Rev r),(len CR),1 = Rev (((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1)) by A11, JORDAN3:def 1
.= Rev (((Rev r) /^ 0 ) | (len CR)) by A12, NAT_2:10
.= Rev ((Rev r) | (len CR)) by FINSEQ_5:31
.= (Rev (Rev r)) /^ ((len (Rev r)) -' (len CR)) by A9, A13, FINSEQ_6:91
.= r /^ ((len r) -' (len CR)) by A3, FINSEQ_6:29 ;
then A14: ovlpart r,CR = ovlpart ((r | ((len r) -' (len CR))) ^ CR),CR by A10, RFINSEQ:21
.= CR by FINSEQ_8:14 ;
ovlcon r,CR = r ^ (CR /^ (len (ovlpart r,CR))) by FINSEQ_8:def 3
.= r ^ {} by A14, REVROT_1:2
.= r by FINSEQ_1:47 ;
hence r = addcr r,CR by FINSEQ_8:def 11; :: thesis: verum

end;

case len CR <= 1 ; :: thesis: r = addcr r,CR

then A15: CR = mid r,(((len r) + 1) -' 1),(len r) by A7, A8, XXREAL_0:1
.= mid r,(len r),(len r) by NAT_D:34
.= r /^ ((len r) -' 1) by JORDAN3:26 ;
A16: CR /^ (len CR) = {} by REVROT_1:2;
A17: r = (r | ((len r) -' 1)) ^ CR by A15, RFINSEQ:21;
ovlcon r,CR = r ^ (CR /^ (len (ovlpart r,CR))) by FINSEQ_8:def 3
.= r ^ (CR /^ (len CR)) by A17, FINSEQ_8:14
.= r by A16, FINSEQ_1:47 ;
hence r = addcr r,CR by FINSEQ_8:def 11; :: thesis: verum

end;

end;

end;

hence r = addcr r,CR ; :: thesis: verum

end;

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

then len CR = 0 by NAT_1:2;
then A18: CR = {} ;
then A19: len (ovlpart r,CR) = len (<*> D) by Th22
.= 0 ;
thus addcr r,CR = ovlcon r,CR by FINSEQ_8:def 11
.= r ^ (CR /^ (len (ovlpart r,CR))) by FINSEQ_8:def 3
.= r ^ CR by A19, FINSEQ_5:31
.= r by A18, FINSEQ_1:47 ; :: thesis: verum

end;

end;