let i, j be Element of NAT ; :: thesis: (F₁() * <:<*F₂()*>:>) . <*i,j*> = F₃(F₄(i,j))
A3: dom <:<*F₂()*>:> = dom F₂() by FUNCT_6:61;
arity F₂() = 2 by Def26;
then A4: dom F₂() = 2 -tuples_on NAT by Th26;
A5: <*i,j*> is Element of 2 -tuples_on NAT by FINSEQ_2:121;
hence (F₁() * <:<*F₂()*>:>) . <*i,j*> = F₁() . (<:<*F₂()*>:> . <*i,j*>) by A3, A4, FUNCT_1:23
.= F₁() . <*(F₂() . <*i,j*>)*> by A4, A5, FUNCT_6:61
.= F₁() . <*F₄(i,j)*> by A2
.= F₃(F₄(i,j)) by A1 ;
:: thesis: verum