let n be natural number ; :: thesis: ( n is finite & card n is finite )
reconsider n = n as Element of omega by ORDINAL1:def 13;
( rng (id n) = n & dom (id n) = n ) by RELAT_1:71;
then n is finite by FINSET_1:def 1;
hence ( n is finite & card n is finite ) by Def5; :: thesis: verum