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