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:28;
for j being Element of NAT st j >= 1 & j > 0 & f is_preposition_of f /^ (j -' 1) holds
j >= 1 ;
hence f is_terminated_by f by A1, A2, Def10; :: thesis: verum