for F being NAT -defined finite initial Function
for n being Nat holds
( n in dom F iff n < card F ) by Lm1;