take f = 0 .--> 0; :: thesis: ( f is NAT -defined & f is finite & not f is empty )
thus dom f c= NAT by ZFMISC_1:31; :: according to RELAT_1:def 18 :: thesis: ( f is finite & not f is empty )
thus ( f is finite & not f is empty ) ; :: thesis: verum