:: deftheorem defines ==>. PRELAMB:def 17 :
for s being non empty typestr
for f being FinSequence of s
for x being type of s holds
( f ==>. x iff [f,x] in the derivability of s );