:: deftheorem Def12 defines initial AFINSQ_1:def 12 :
for F being Function holds
( F is initial iff for m, n being Nat st n in dom F & m < n holds
m in dom F );