:: deftheorem defines is_preposition_of FINSEQ_8:def 8 :
for g, f being FinSequence holds
( g is_preposition_of f iff ( len g > 0 implies ( 1 <= len f & mid (f,1,(len g)) = g ) ) );