deffunc H1( FinSequence of NAT ) -> Element of HFuncs NAT = primrec (f1,f2,i,$1);
reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th27;
set n = (arity f1) + 1;
consider G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that
A1:
for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = H1(p)
from FUNCT_2:sch 4();
reconsider Y = rng G as non empty Subset of (HFuncs NAT) by RELAT_1:def 19;
Y is PartFunc-set of NAT * , NAT
then reconsider Y = Y as PFUNC_DOMAIN of NAT * , NAT ;
A2:
Y is compatible
proof
let f,
g be
Function;
COMPUT_1:def 1 ( f in Y & g in Y implies f tolerates g )
assume
f in Y
;
( not g in Y or f tolerates g )
then consider x being
object such that A3:
x in dom G
and A4:
f = G . x
by FUNCT_1:def 3;
assume
g in Y
;
f tolerates g
then consider y being
object such that A5:
y in dom G
and A6:
g = G . y
by FUNCT_1:def 3;
reconsider x =
x,
y =
y as
Element of
((arity f1) + 1) -tuples_on NAT by A3, A5;
A7:
g = primrec (
ff1,
ff2,
i,
y)
by A1, A6;
f = primrec (
ff1,
ff2,
i,
x)
by A1, A4;
hence
f tolerates g
by A7, Th50;
verum
end;
then consider g being Element of HFuncs NAT such that
A8:
g = Union G
and
dom g c= ((arity f1) + 1) -tuples_on NAT
by A2, Th38;
take
g
; ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
take
G
; ( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
thus
( g = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
by A1, A8; verum