scheme :: COMPUT_1:sch 1
Primrec1{ F₁() -> NAT * -defined to-naturals homogeneous len-total 1 -ary Function, F₂() -> NAT * -defined to-naturals homogeneous len-total 2 -ary Function, F₃( set ) -> Nat, F₄( set , set ) -> Nat } :

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

provided

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