let D be non empty set ; :: thesis: for f, g being FinSequence of D
for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds
g is_substring_of f,1
let f, g be FinSequence of D; :: thesis: for n being Element of NAT st g is_substring_of f | n,1 & len g > 0 holds
g is_substring_of f,1
let n be Element of NAT ; :: thesis: ( g is_substring_of f | n,1 & len g > 0 implies g is_substring_of f,1 )
assume that
A1: g is_substring_of f | n,1 and
A2: len g > 0 ; :: thesis: g is_substring_of f,1
consider i2 being Nat such that
A3: 1 <= i2 and
A4: i2 <= len (f | n) and
A5: mid ((f | n),i2,((i2 -' 1) + (len g))) = g by A1, A2, FINSEQ_8:def 7;
len g >= 0 + 1 by A2, NAT_1:13;
then (len g) - 1 >= 0 by XREAL_1:48;
then A6: ((len g) - 1) + i2 >= 0 + i2 by XREAL_1:7;
then A7: (i2 - 1) + (len g) >= i2 ;

per cases ( len f >= n or len f < n ) ;

suppose A8: len f >= n ; :: thesis: g is_substring_of f,1

(i2 -' 1) + (len g) = (i2 - 1) + (len g) by A3, XREAL_1:233;
then A9: (((i2 -' 1) + (len g)) -' i2) + 1 = (((i2 - 1) + (len g)) - i2) + 1 by A6, XREAL_1:233
.= len g ;
i2 - 1 >= 0 by A3, XREAL_1:48;
then A10: i2 <= (i2 -' 1) + (len g) by A7, XREAL_0:def 2;
then A11: g = ((f | n) /^ (i2 -' 1)) | ((((i2 -' 1) + (len g)) -' i2) + 1) by A5, FINSEQ_6:def 3
.= ((f /^ (i2 -' 1)) | (n -' (i2 -' 1))) | (len g) by A9, FINSEQ_5:80 ;

now :: thesis: not n -' (i2 -' 1) < len g

A12: len (f /^ (i2 -' 1)) = (len f) -' (i2 -' 1) by RFINSEQ:29;
assume A13: n -' (i2 -' 1) < len g ; :: thesis: contradiction
then g = (f /^ (i2 -' 1)) | (n -' (i2 -' 1)) by A11, FINSEQ_5:77;
hence contradiction by A8, A13, A12, FINSEQ_1:59, NAT_D:42; :: thesis: verum

end;

then A14: g = (f /^ (i2 -' 1)) | (len g) by A11, FINSEQ_5:77
.= mid (f,i2,((i2 -' 1) + (len g))) by A10, A9, FINSEQ_6:def 3 ;
len (f | n) <= len f by FINSEQ_5:16;
then i2 <= len f by A4, XXREAL_0:2;
hence g is_substring_of f,1 by A3, A14, FINSEQ_8:def 7; :: thesis: verum

end;

suppose len f < n ; :: thesis: g is_substring_of f,1

hence g is_substring_of f,1 by A1, FINSEQ_1:58; :: thesis: verum

end;

end;