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 & len g <= n 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 & len g <= n holds
g is_substring_of f,1
let n be Element of NAT ; :: thesis: ( g is_substring_of f | n,1 & len g > 0 & len g <= n implies g is_substring_of f,1 )
assume A1: ( g is_substring_of f | n,1 & len g > 0 & len g <= n ) ; :: thesis: g is_substring_of f,1
then len g >= 0 + 1 by NAT_1:13;
then A2: (len g) - 1 >= 0 by XREAL_1:50;
consider i2 being Element of NAT such that
A3: ( 1 <= i2 & i2 <= len (f | n) & mid (f | n),i2,((i2 -' 1) + (len g)) = g ) by A1, FINSEQ_8:def 7;
A4: ((len g) - 1) + i2 >= 0 + i2 by A2, XREAL_1:9;
then A5: (i2 - 1) + (len g) >= i2 ;

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

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

i2 - 1 >= 0 by A3, XREAL_1:50;
then A7: i2 <= (i2 -' 1) + (len g) by A5, XREAL_0:def 2;
(i2 -' 1) + (len g) = (i2 - 1) + (len g) by A3, XREAL_1:235;
then A8: (((i2 -' 1) + (len g)) -' i2) + 1 = (((i2 - 1) + (len g)) - i2) + 1 by A4, XREAL_1:235
.= len g ;
A9: g = ((f | n) /^ (i2 -' 1)) | ((((i2 -' 1) + (len g)) -' i2) + 1) by A3, A7, JORDAN3:def 1
.= ((f /^ (i2 -' 1)) | (n -' (i2 -' 1))) | (len g) by A8, JORDAN3:21 ;

now

assume A10: n -' (i2 -' 1) < len g ; :: thesis: contradiction
then A11: g = (f /^ (i2 -' 1)) | (n -' (i2 -' 1)) by A9, FINSEQ_5:80;
len (f /^ (i2 -' 1)) = (len f) -' (i2 -' 1) by JORDAN3:19;
hence contradiction by A6, A10, A11, FINSEQ_1:80, NAT_D:42; :: thesis: verum

end;

then A12: g = (f /^ (i2 -' 1)) | (len g) by A9, FINSEQ_5:80
.= mid f,i2,((i2 -' 1) + (len g)) by A7, A8, JORDAN3:def 1 ;
len (f | n) <= len f by FINSEQ_5:18;
then ( 1 <= i2 & i2 <= len f & mid f,i2,((i2 -' 1) + (len g)) = g ) by A3, A12, XXREAL_0:2;
hence g is_substring_of f,1 by 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:79; :: thesis: verum

end;

end;