let P be non empty primitive-recursively_closed Subset of (HFuncs NAT ); :: thesis: for f1, f2 being Element of P st (arity f1) + 2 = arity f2 holds
for i being Element of NAT st 1 <= i & i <= (arity f1) + 1 holds
primrec f1,f2,i in P
let f1, f2 be Element of P; :: thesis: ( (arity f1) + 2 = arity f2 implies for i being Element of NAT st 1 <= i & i <= (arity f1) + 1 holds
primrec f1,f2,i in P )
assume A1: (arity f1) + 2 = arity f2 ; :: thesis: for i being Element of NAT st 1 <= i & i <= (arity f1) + 1 holds
primrec f1,f2,i in P
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (arity f1) + 1 implies primrec f1,f2,i in P )
assume A2: ( 1 <= i & i <= (arity f1) + 1 ) ; :: thesis: primrec f1,f2,i in P
A3: P is primitive-recursion_closed by Def17;

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

suppose f1 is empty ; :: thesis: primrec f1,f2,i in P

then primrec f1,f2,i is empty by Th59;
hence primrec f1,f2,i in P by Th75; :: thesis: verum

end;

suppose not f1 is empty ; :: thesis: primrec f1,f2,i in P

then primrec f1,f2,i is_primitive-recursively_expressed_by f1,f2,i by A1, A2, Th21, Th68;
hence primrec f1,f2,i in P by A3, Def16; :: thesis: verum

end;

end;