let i be 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 object ; :: 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 Def11;
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 that
A5: f in rng G and
A6: g in rng G ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: for x being Element of ((arity f1) + 1) -tuples_on NAT holds dom (G . x) c= ((arity f1) + 1) -tuples_on NAT

let x be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: dom (G . x) c= ((arity f1) + 1) -tuples_on NAT
G . x = primrec (f1,f2,i,x) by A3;
hence dom (G . x) c= ((arity f1) + 1) -tuples_on NAT by Th51; :: thesis: 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; :: thesis: verum