theorem :: AFINSQ_1:68

for F being NAT -defined finite initial Function holds dom F = { k where k is Element of NAT : k < card F }