let a, b, c be Element of [:F_{1}(),F_{2}():]; :: thesis: P_{1}[a,b,c]

A2: ex b1 being Element of F_{1}() ex b2 being Element of F_{2}() st b = [b1,b2]
by DOMAIN_1:1;

A3: ex c1 being Element of F_{1}() ex c2 being Element of F_{2}() st c = [c1,c2]
by DOMAIN_1:1;

ex a1 being Element of F_{1}() ex a2 being Element of F_{2}() st a = [a1,a2]
by DOMAIN_1:1;

hence P_{1}[a,b,c]
by A1, A2, A3; :: thesis: verum

A2: ex b1 being Element of F

A3: ex c1 being Element of F

ex a1 being Element of F

hence P