let D be non empty set ; :: thesis: for f, g being FinSequence of D st g is_postposition_of f & len g > 0 holds
( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g )
let f, g be FinSequence of D; :: thesis: ( g is_postposition_of f & len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) )
assume A1: g is_postposition_of f ; :: thesis: ( not len g > 0 or ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) )
then A2: Rev g is_preposition_of Rev f ;
then A3: ( len (Rev g) > 0 implies ( 1 <= len (Rev f) & mid ((Rev f),1,(len (Rev g))) = Rev g ) ) ;
A5: len (Rev f) = len f by FINSEQ_5:def 3;

now :: thesis: ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) )

assume A6: len g > 0 ; :: thesis: ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g )
then A7: 1 <= len f by A2, FINSEQ_5:def 3;
A8: mid ((Rev f),1,(len g)) = Rev g by A2, FINSEQ_5:def 3, A6;
A9: (len f) - 1 >= 0 by A3, A5, A6, FINSEQ_5:def 3, XREAL_1:48;
A10: len g <= len f by A1, Th23;
A11: (len f) - (len g) >= 0 by A1, Th23, XREAL_1:48;
len f < (len f) + 1 by XREAL_1:29;
then len g < (len f) + 1 by A10, XXREAL_0:2;
then A12: ((len f) + 1) - (len g) > 0 by XREAL_1:50;
A13: 0 + 1 <= len g by A6, NAT_1:13;
A14: g = Rev (Rev g)
.= mid ((Rev (Rev f)),(((len f) -' (len g)) + 1),(((len f) -' 1) + 1)) by A5, A7, A8, A10, A13, FINSEQ_6:113
.= mid (f,(((len f) -' (len g)) + 1),(((len f) -' 1) + 1)) ;
A15: ((len f) -' (len g)) + 1 = ((len f) - (len g)) + 1 by A11, XREAL_0:def 2
.= ((len f) + 1) -' (len g) by A12, XREAL_0:def 2 ;
((len f) -' 1) + 1 = ((len f) - 1) + 1 by A9, XREAL_0:def 2
.= len f ;
hence ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) by A1, A14, A15, Th23; :: thesis: verum

end;

hence ( not len g > 0 or ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) ; :: thesis: verum