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:66;
set f = 0 const 0;
A1: rng {} c= P by XBOOLE_1:2;
A2: arity (0 const 0) = 0 by Th35;
A3: P is composition_closed by Def17;
0 const 0 in P by Th73;
then (0 const 0) * <:F:> in P by A2, A1, A3, Def15, CARD_1:47;
hence {} in P by FUNCT_6:60; :: thesis: verum