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