theorem Th62: :: AFINSQ_1:65

for F being NAT -defined non empty initial Function holds 0 in dom F