let P be non empty primitive-recursively_closed Subset of (HFuncs NAT); :: thesis: {} in P
reconsider F = {} as with_the_same_arity Element of (HFuncs NAT) * by FINSEQ_1:49;
set f = 0 const 0;
A1: rng {} c= P ;
A2: arity (0 const 0) = 0 by Th31;
A3: P is composition_closed by Def14;
0 const 0 in P by Th68;
then (0 const 0) * <:F:> in P by A2, A1, A3, CARD_1:27;
hence {} in P by FUNCT_6:40; :: thesis: verum