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 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 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 Nat st 1 <= i & i <= (arity f1) + 1 holds
primrec (f1,f2,i) in P
let i be Nat; :: thesis: ( 1 <= i & i <= (arity f1) + 1 implies primrec (f1,f2,i) in P )
assume that
A2: 1 <= i and
A3: i <= (arity f1) + 1 ; :: thesis: primrec (f1,f2,i) in P
A4: P is primitive-recursion_closed by Def14;

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 Th54;
hence primrec (f1,f2,i) in P by Th70; :: 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, A3, Th17, Th63;
hence primrec (f1,f2,i) in P by A4; :: thesis: verum

end;

end;