let n be Nat; :: thesis: ( n is finite & card n is finite )
reconsider n = n as Element of omega by ORDINAL1:def 12;
( rng (id n) = n & dom (id n) = n ) by RELAT_1:45;
hence ( n is finite & card n is finite ) ; :: thesis: verum