let a, b, c be Element of [:F1(),F2():]; P1[a,b,c]
A2:
ex b1 being Element of F1() ex b2 being Element of F2() st b = [b1,b2]
by DOMAIN_1:1;
A3:
ex c1 being Element of F1() ex c2 being Element of F2() st c = [c1,c2]
by DOMAIN_1:1;
ex a1 being Element of F1() ex a2 being Element of F2() st a = [a1,a2]
by DOMAIN_1:1;
hence
P1[a,b,c]
by A1, A2, A3; verum