let P be non empty primitive-recursively_closed Subset of (HFuncs NAT); 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; ( (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
; 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 ; ( 1 <= i & i <= (arity f1) + 1 implies primrec (f1,f2,i) in P )
assume that
A2:
1 <= i
and
A3:
i <= (arity f1) + 1
; 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
not
f1 is
empty
;
primrec (f1,f2,i) in Pthen
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;
verum end; end;