let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= len f holds
f is_substring_of f,1
let f be FinSequence of D; :: thesis: ( 1 <= len f implies f is_substring_of f,1 )
assume A1: 1 <= len f ; :: thesis: f is_substring_of f,1
(1 -' 1) + (len f) = 0 + (len f) by NAT_2:10
.= len f ;
then mid f,1,((1 -' 1) + (len f)) = f by A1, FINSEQ_6:126;
hence f is_substring_of f,1 by A1, Def7; :: thesis: verum