scheme :: COMPUT_1:sch 2
Primrec2{ F₁() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F₂() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F₃() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F₄( set , set ) -> Element of NAT , F₅( set , set ) -> Element of NAT , F₆( set , set ) -> Element of NAT } :

for i, j being Element of NAT holds (F₁() * <:<*F₂(),F₃()*>:>) . <*i,j*> = F₄(F₅(i,j),F₆(i,j))

provided

A1: for i, j being Element of NAT holds F₁() . <*i,j*> = F₄(i,j) and
A2: for i, j being Element of NAT holds F₂() . <*i,j*> = F₅(i,j) and
A3: for i, j being Element of NAT holds F₃() . <*i,j*> = F₆(i,j)