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) )
A1: len r = len (Rev r) by FINSEQ_5:def 3;
assume A2: CR is_postposition_of r ; :: thesis: r = addcr (r,CR)
then A3: ( len CR = len (Rev CR) & Rev CR is_preposition_of Rev r ) by FINSEQ_5:def 3, FINSEQ_8:def 9;
0 <= (len r) - (len CR) by A2, Th26;
then A4: 0 + (len CR) <= ((len r) - (len CR)) + (len CR) by XREAL_1:7;

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

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

then Rev (mid ((Rev r),1,(len CR))) = Rev (Rev CR) by A3, FINSEQ_8:def 8;
then A6: mid ((Rev r),(len CR),1) = Rev (Rev CR) by FINSEQ_6:196
.= CR ;
A7: len (Rev r) = ((len (Rev r)) - (len CR)) + (len CR) ;
A8: ( mid (r,(((len r) + 1) -' (len CR)),(len r)) = CR & len CR >= 0 + 1 ) by A2, A5, FINSEQ_8:24, NAT_1:13;

now :: thesis: ( ( len CR > 1 & r = addcr (r,CR) ) or ( len CR <= 1 & r = addcr (r,CR) ) )

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

case A9: 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:9;
then A10: ((len CR) -' 1) + 1 = len CR by NAT_D:43;
A11: (len (Rev r)) -' (len CR) = (len (Rev r)) - (len CR) by A1, A4, XREAL_1:233;
mid ((Rev r),(len CR),1) = Rev (((Rev r) /^ (1 -' 1)) | (((len CR) -' 1) + 1)) by A9, FINSEQ_6:def 3
.= Rev (((Rev r) /^ 0) | (len CR)) by A10, NAT_2:8
.= Rev ((Rev r) | (len CR))
.= (Rev (Rev r)) /^ ((len (Rev r)) -' (len CR)) by A7, A11, FINSEQ_6:85
.= r /^ ((len r) -' (len CR)) by A1 ;
then A12: ovlpart (r,CR) = ovlpart (((r | ((len r) -' (len CR))) ^ CR),CR) by A6, RFINSEQ:8
.= CR by FINSEQ_8:14 ;
ovlcon (r,CR) = r ^ (CR /^ (len (ovlpart (r,CR)))) by FINSEQ_8:def 3
.= r ^ {} by A12, FINSEQ_6:167
.= r by FINSEQ_1:34 ;
hence r = addcr (r,CR) by FINSEQ_8:def 11; :: thesis: verum

end;

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

then CR = mid (r,(((len r) + 1) -' 1),(len r)) by A8, XXREAL_0:1
.= mid (r,(len r),(len r)) by NAT_D:34
.= r /^ ((len r) -' 1) by FINSEQ_6:117 ;
then A13: r = (r | ((len r) -' 1)) ^ CR by RFINSEQ:8;
A14: CR /^ (len CR) = {} by FINSEQ_6:167;
ovlcon (r,CR) = r ^ (CR /^ (len (ovlpart (r,CR)))) by FINSEQ_8:def 3
.= r ^ (CR /^ (len CR)) by A13, FINSEQ_8:14
.= r by A14, FINSEQ_1:34 ;
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 A15: CR = {} ;
then A16: len (ovlpart (r,CR)) = len (<*> D) by Th21
.= 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 A16
.= r by A15, FINSEQ_1:34 ; :: thesis: verum

end;

end;