let i, j be Element of NAT ; (F1() * <:<*F2()*>:>) . <*i,j*> = F3(F4(i,j))
arity F2() = 2
by Def21;
then A3:
dom F2() = 2 -tuples_on NAT
by Th22;
dom <:<*F2()*>:> = dom F2()
by FINSEQ_3:141;
hence (F1() * <:<*F2()*>:>) . <*i,j*> =
F1() . (<:<*F2()*>:> . <*i,j*>)
by A3, FINSEQ_2:101, FUNCT_1:13
.=
F1() . <*(F2() . <*i,j*>)*>
by A3, FINSEQ_2:101, FINSEQ_3:141
.=
F1() . <*F4(i,j)*>
by A2
.=
F3(F4(i,j))
by A1
;
verum