let f be FinSequence; :: 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:8
.= len f ;
then mid (f,1,((1 -' 1) + (len f))) = f by A1, FINSEQ_6:120;
hence f is_substring_of f,1 by A1; :: thesis: verum