A3:
F2() = { [o,F4(o)] where o is Element of F1() : P1[o] }
by A1;
dom F2() = { o where o is Element of F1() : P1[o] }
from ALTCAT_2:sch 2(A3);
then A4:
F3() in dom F2()
by A2;
[F3(),F4(F3())] in { [o,F4(o)] where o is Element of F1() : P1[o] }
by A2;
hence
F2() . F3() = F4(F3())
by A1, A4, FUNCT_1:def 2; verum