let P be non empty primitive-recursively_closed Subset of (HFuncs NAT ); :: thesis: {} in P
set f = 0 const 0 ;
A1: 0 const 0 in P by Th73;
A3: arity (0 const 0 ) = 0 by Th35;
A4: rng {} c= P by XBOOLE_1:2;
reconsider F = {} as with_the_same_arity Element of (HFuncs NAT ) * by FINSEQ_1:66;
P is composition_closed by Def17;
then (0 const 0 ) * <:F:> in P by A1, A3, A4, Def15, CARD_1:47;
then (0 const 0 ) * {} in P by FUNCT_6:60;
hence {} in P ; :: thesis: verum