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 f is_preposition_of by Def9;
then A3: ( len (Rev g) > 0 implies ( 1 <= len (Rev f) & mid (Rev f),1,(len (Rev g)) = Rev g ) ) by Def8;
A4: len (Rev g) = len g by FINSEQ_5:def 3;
A5: len (Rev f) = len f by FINSEQ_5:def 3;

now

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, A4, A5, Def8;
A8: mid (Rev f),1,(len g) = Rev g by A2, A4, A6, Def8;
A9: (len f) - 1 >= 0 by A3, A5, A6, FINSEQ_5:def 3, XREAL_1:50;
A10: len g <= len f by A1, Th23;
A11: (len f) - (len g) >= 0 by A1, Th23, XREAL_1:50;
len f < (len f) + 1 by XREAL_1:31;
then len g < (len f) + 1 by A10, XXREAL_0:2;
then A12: ((len f) + 1) - (len g) > 0 by XREAL_1:52;
A13: 0 + 1 <= len g by A6, NAT_1:13;
A14: g = Rev (Rev g) by FINSEQ_6:29
.= mid (Rev (Rev f)),(((len f) -' (len g)) + 1),(((len f) -' 1) + 1) by A5, A7, A8, A10, A13, JORDAN3:22
.= mid f,(((len f) -' (len g)) + 1),(((len f) -' 1) + 1) by FINSEQ_6:29 ;
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