let f, g be FinSequence; :: 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 :: thesis: ( ( len g > 0 & g is_substring_of f,1 ) or ( len g <= 0 & g is_substring_of f,1 ) )

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 Nat such that
0 <= i and
A3: i <= len f and
A4: mid (f,i,((i -' 1) + (len g))) = g by A1;
A5: len g >= 0 + 1 by A2, NAT_1:13;

now :: thesis: ( ( i = 0 & g is_substring_of f,1 ) or ( i <> 0 & g is_substring_of f,1 ) )

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, FINSEQ_6:def 3;
(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:28;

now :: thesis: ( ( (len g) + 1 >= len f & g is_substring_of f,1 ) or ( (len g) + 1 < len f & contradiction ) )

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:58;
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:61
.= (Seg (len f)) /\ (Seg ((len g) + 1)) by FINSEQ_1:def 3
.= Seg ((len g) + 1) by A10, FINSEQ_1:7 ;
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; :: 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 ; :: thesis: verum

end;

end;

end;

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