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;
end;
end;
hence g is_substring_of f,1 ; :: thesis: verum