let D be non empty set ; :: thesis: for f, g being FinSequence of D st g is_substring_of f, 0 holds
g is_substring_of f,1
let f, g be FinSequence of D; :: thesis: ( g is_substring_of f, 0 implies g is_substring_of f,1 )
assume A1: g is_substring_of f, 0 ; :: thesis: g is_substring_of f,1

now

per cases ( len g > 0 or len g <= 0 ) ;

case A2: len g > 0 ; :: thesis: g is_substring_of f,1

then consider i being Element of NAT such that
0 <= i and
A3: i <= len f and
A4: mid f,i,((i -' 1) + (len g)) = g by A1, Def7;
A5: len g >= 0 + 1 by A2, NAT_1:13;

now

per cases ( i = 0 or i <> 0 ) ;

case A6: i = 0 ; :: thesis: g is_substring_of f,1

0 - 1 < 0 ;
then A7: i -' 1 = 0 by A6, XREAL_0:def 2;
then A8: (f /^ (0 -' 1)) | (((len g) -' 0 ) + 1) = g by A4, A6, JORDAN3:def 1;
(len g) -' 0 = (len g) - 0 by XREAL_0:def 2
.= len g ;
then A9: f | ((len g) + 1) = g by A6, A7, A8, FINSEQ_5:31;

now

per cases ( (len g) + 1 >= len f or (len g) + 1 < len f ) ;

case (len g) + 1 >= len f ; :: thesis: g is_substring_of f,1

then f = g by A9, FINSEQ_1:79;
hence g is_substring_of f,1 by A5, Th19; :: thesis: verum

end;

case A10: (len g) + 1 < len f ; :: thesis: contradiction

dom (f | (Seg ((len g) + 1))) = (dom f) /\ (Seg ((len g) + 1)) by RELAT_1:90
.= (Seg (len f)) /\ (Seg ((len g) + 1)) by FINSEQ_1:def 3
.= Seg ((len g) + 1) by A10, FINSEQ_1:9 ;
then len g = (len g) + 1 by A9, FINSEQ_1:def 3;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence g is_substring_of f,1 ; :: thesis: verum

end;

case i <> 0 ; :: thesis: g is_substring_of f,1

then i >= 0 + 1 by NAT_1:13;
hence g is_substring_of f,1 by A3, A4, Def7; :: thesis: verum

end;

end;

end;

hence g is_substring_of f,1 ; :: thesis: verum

end;

case len g <= 0 ; :: thesis: g is_substring_of f,1

hence g is_substring_of f,1 by Def7; :: thesis: verum

end;

end;

end;

hence g is_substring_of f,1 ; :: thesis: verum