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