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

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