let D be non empty set ; :: thesis: for f, g being FinSequence of D st 1 <= len f & f is_preposition_of holds
g is_substring_of f,1
let f, g be FinSequence of D; :: thesis: ( 1 <= len f & f is_preposition_of implies g is_substring_of f,1 )
assume that
A1: 1 <= len f and
A2: f is_preposition_of ; :: thesis: g is_substring_of f,1

now

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:10
.= g by A2, A3, Def8 ;
hence g is_substring_of f,1 by A1, Def7; :: thesis: verum

end;

case len g <= 0 ; :: thesis: g is_substring_of f,1

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

end;

end;

end;

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