let i be Element of NAT ; :: thesis: 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; :: thesis: dom (primrec f1,f2,i) c= ((arity f1) + 1) -tuples_on NAT
let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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)
; :: thesis: 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 Def14;
A4:
rng G is compatible
proof
let f,
g be
Function;
:: according to COMPUT_1:def 1 :: thesis: ( f in rng G & g in rng G implies f tolerates g )
assume A5:
(
f in rng G &
g in rng G )
;
:: thesis: f tolerates g
consider fx being
set such that A6:
(
fx in dom G &
f = G . fx )
by A5, FUNCT_1:def 5;
consider gx being
set such that A7:
(
gx in dom G &
g = G . gx )
by A5, FUNCT_1:def 5;
reconsider fx =
fx as
Element of
((arity f1) + 1) -tuples_on NAT by A6;
reconsider gx =
gx as
Element of
((arity f1) + 1) -tuples_on NAT by A7;
(
G . fx = primrec f1,
f2,
i,
fx &
G . gx = primrec f1,
f2,
i,
gx )
by A3;
hence
f tolerates g
by A6, A7, Th55;
:: thesis: verum
end;
then consider F being Element of HFuncs NAT such that
A8:
( F = Union G & dom F c= ((arity f1) + 1) -tuples_on NAT )
by A4, Th43;
thus
x in ((arity f1) + 1) -tuples_on NAT
by A1, A2, A8; :: thesis: verum