let D be non empty set ; 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; ( 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
; ( 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 ( len g > 0 implies ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) )assume A6:
len g > 0
;
( 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;
verum end;
hence
( not len g > 0 or ( len g <= len f & mid (f,(((len f) + 1) -' (len g)),(len f)) = g ) )
; verum