let i be Element of NAT ; for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function holds dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT
let x be object ; TARSKI:def 3 ( not x in dom (primrec (f1,f2,i)) or x in ((arity f1) + 1) -tuples_on NAT )
assume A1:
x in dom (primrec (f1,f2,i))
; x in ((arity f1) + 1) -tuples_on NAT
consider G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that
A2:
primrec (f1,f2,i) = Union G
and
A3:
for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p)
by Def11;
A4:
rng G is compatible
proof
let f,
g be
Function;
COMPUT_1:def 1 ( f in rng G & g in rng G implies f tolerates g )
assume that A5:
f in rng G
and A6:
g in rng G
;
f tolerates g
consider fx being
object such that A7:
fx in dom G
and A8:
f = G . fx
by A5, FUNCT_1:def 3;
reconsider fx =
fx as
Element of
((arity f1) + 1) -tuples_on NAT by A7;
consider gx being
object such that A9:
gx in dom G
and A10:
g = G . gx
by A6, FUNCT_1:def 3;
reconsider gx =
gx as
Element of
((arity f1) + 1) -tuples_on NAT by A9;
A11:
G . gx = primrec (
f1,
f2,
i,
gx)
by A3;
G . fx = primrec (
f1,
f2,
i,
fx)
by A3;
hence
f tolerates g
by A8, A10, A11, Th50;
verum
end;
then
ex F being Element of HFuncs NAT st
( F = Union G & dom F c= ((arity f1) + 1) -tuples_on NAT )
by A4, Th38;
hence
x in ((arity f1) + 1) -tuples_on NAT
by A1, A2; verum