let D be non empty set ; :: thesis: for f being FinSequence of D holds f is_terminated_by f
let f be FinSequence of D; :: thesis: f is_terminated_by f
A1: ((len f) + 1) -' (len f) = ((len f) + 1) - (len f) by XREAL_0:def 2;
1 -' 1 = (0 + 1) -' 1
.= 0 by NAT_D:34 ;
then A2: f /^ (1 -' 1) = f by FINSEQ_5:31;
for j being Element of NAT st j >= 1 & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= 1 ;
then instr (1,f,f) = ((len f) + 1) -' (len f) by A1, A2, Def10;
hence f is_terminated_by f by Def12; :: thesis: verum