let i, j be Element of NAT ; :: thesis: (F₁() * <:<*F₂(),F₃()*>:>) . <*i,j*> = F₄(F₅(i,j),F₆(i,j))
arity F₂() = 2 by Def21;
then A4: dom F₂() = 2 -tuples_on NAT by Th22;
arity F₃() = 2 by Def21;
then A5: dom F₃() = 2 -tuples_on NAT by Th22;
B1: ( F₅(i,j) in NAT & F₆(i,j) in NAT ) by ORDINAL1:def 12;
A6: dom <:<*F₂(),F₃()*>:> = (dom F₂()) /\ (dom F₃()) by FINSEQ_3:142;
hence (F₁() * <:<*F₂(),F₃()*>:>) . <*i,j*> = F₁() . (<:<*F₂(),F₃()*>:> . <*i,j*>) by A4, A5, FINSEQ_2:101, FUNCT_1:13
.= F₁() . <*(F₂() . <*i,j*>),(F₃() . <*i,j*>)*> by A6, A4, A5, FINSEQ_2:101, FINSEQ_3:142
.= 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, B1 ;
:: thesis: verum