take f = 0 .--> 0 ; :: thesis: ( f is NAT -defined & f is finite & not f is empty )
X: 0 in NAT ;
dom f = {0 } by FUNCOP_1:19;
hence dom f c= NAT by X, ZFMISC_1:37; :: according to RELAT_1:def 18 :: thesis: ( f is finite & not f is empty )
thus ( f is finite & not f is empty ) ; :: thesis: verum