let D be non empty set ; :: thesis: for f, g being FinSequence of D st ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) holds
g is_postposition_of f
let f, g be FinSequence of D; :: thesis: ( ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) implies g is_postposition_of f )
assume A1: ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) ) ; :: thesis: g is_postposition_of f
A2: len (Rev f) = len f by FINSEQ_5:def 3;
now :: thesis: ( ( len g > 0 & g is_postposition_of f ) or ( len g <= 0 & g is_postposition_of f ) )
per cases ( len g > 0 or len g <= 0 ) ;
case A3: len g > 0 ; :: thesis: g is_postposition_of f
then A4: 0 + 1 <= len g by NAT_1:13;
then A5: (len g) - 1 >= 0 by XREAL_1:48;
len f < (len f) + 1 by XREAL_1:29;
then a6: len g < (len f) + 1 by A1, XXREAL_0:2;
then A6: ((len f) + 1) - (len g) > 0 by XREAL_1:50;
then ((len f) + 1) -' (len g) = ((len f) + 1) - (len g) by XREAL_0:def 2;
then A7: 0 + 1 <= ((len f) + 1) -' (len g) by a6, NAT_1:13, XREAL_1:50;
A8: ((len f) + 1) -' (len g) = (len f) - ((len g) - 1) by A6, XREAL_0:def 2;
(len f) + 0 <= (len f) + ((len g) - 1) by A5, XREAL_1:7;
then A9: (len f) - ((len g) - 1) <= len f by XREAL_1:20;
A10: 1 <= len f by A1, A4, XXREAL_0:2;
A11: ((len f) -' (len f)) + 1 = ((len f) - (len f)) + 1 by XREAL_0:def 2
.= 1 ;
len f < (len f) + 1 by XREAL_1:29;
then len g <= (len f) + 1 by A1, XXREAL_0:2;
then A12: (len f) - (((len f) + 1) -' (len g)) = (len f) - (((len f) + 1) - (len g)) by XREAL_0:def 2, XREAL_1:48
.= (len g) - 1 ;
then A13: ((len f) -' (((len f) + 1) -' (len g))) + 1 = ((len f) - (((len f) + 1) -' (len g))) + 1 by A5, XREAL_0:def 2;
Rev g = mid ((Rev f),(((len f) -' (len f)) + 1),(((len f) -' (((len f) + 1) -' (len g))) + 1)) by A1, A3, A7, A8, A9, A10, FINSEQ_6:113
.= mid ((Rev f),1,(len (Rev g))) by A11, A12, A13, FINSEQ_5:def 3 ;
then Rev g is_preposition_of Rev f by A1, A2, A4, XXREAL_0:2;
hence g is_postposition_of f ; :: thesis: verum
end;
end;
end;
hence g is_postposition_of f ; :: thesis: verum