let P be non empty primitive-recursively_closed Subset of (HFuncs NAT); :: thesis: for f being Element of P
for F being with_the_same_arity FinSequence of P st arity f = len F holds
f * <:F:> in P
let f be Element of P; :: thesis: for F being with_the_same_arity FinSequence of P st arity f = len F holds
f * <:F:> in P
let F be with_the_same_arity FinSequence of P; :: thesis: ( arity f = len F implies f * <:F:> in P )
assume A1: arity f = len F ; :: thesis: f * <:F:> in P
A2: rng F c= P by FINSEQ_1:def 4;

per cases ( f is empty or not f is empty ) ;

suppose f is empty ; :: thesis: f * <:F:> in P

then f * <:F:> = {} ;
hence f * <:F:> in P by Th70; :: thesis: verum

end;

suppose not f is empty ; :: thesis: f * <:F:> in P

then reconsider f9 = f as non empty Element of HFuncs NAT ;
A3: P * c= (HFuncs NAT) * by FINSEQ_1:62;
F in P * by FINSEQ_1:def 11;
then reconsider F9 = F as with_the_same_arity Element of (HFuncs NAT) * by A3;
P is composition_closed by Def14;
then f9 * <:F9:> in P by A1, A2;
hence f * <:F:> in P ; :: thesis: verum

end;

end;