let D be non empty set ; 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; ( ( 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 ) )
; g is_postposition_of f
A2:
len (Rev f) = len f
by FINSEQ_5:def 3;
now ( ( 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
;
g is_postposition_of fthen 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
;
verum end;
hence
g is_postposition_of f
; verum