take 0 .--> 0 ; :: thesis: ( not 0 .--> 0 is empty & 0 .--> 0 is trivial & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite )
A: dom (0 .--> 0 ) = {0 } by FUNCOP_1:19;
then dom (0 .--> 0 ) c= NAT by ZFMISC_1:37;
then 0 .--> 0 is NAT -defined by RELAT_1:def 18;
hence ( not 0 .--> 0 is empty & 0 .--> 0 is trivial & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite ) ; :: thesis: verum