let i, j be Element of NAT ; :: thesis: (F₁() * <:<*F₂()*>:>) . <*i,j*> = F₃(F₄(i,j))
arity F₂() = 2 by Def21;
then A3: dom F₂() = 2 -tuples_on NAT by Th22;
B1: F₄(i,j) in NAT by ORDINAL1:def 12;
dom <:<*F₂()*>:> = dom F₂() by FINSEQ_3:141;
hence (F₁() * <:<*F₂()*>:>) . <*i,j*> = F₁() . (<:<*F₂()*>:> . <*i,j*>) by A3, FINSEQ_2:101, FUNCT_1:13
.= F₁() . <*(F₂() . <*i,j*>)*> by A3, FINSEQ_2:101, FINSEQ_3:141
.= F₁() . <*F₄(i,j)*> by A2
.= F₃(F₄(i,j)) by A1, B1 ;
:: thesis: verum