let f, g be FinSequence; :: thesis: ( 1 <= len f & g is_preposition_of f implies g is_substring_of f,1 )
assume that
A1: 1 <= len f and
A2: g is_preposition_of f ; :: 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 A3: len g > 0 ; :: thesis: g is_substring_of f,1

mid (f,1,((1 -' 1) + (len g))) = mid (f,1,(0 + (len g))) by NAT_2:8
.= g by A2, A3 ;
hence g is_substring_of f,1 by A1; :: 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