let d, d9 be Element of [:F₁(),F₂():]; :: thesis: P₁[d,d9]
A2: ex d19 being Element of F₁() ex d29 being Element of F₂() st d9 = [d19,d29] by DOMAIN_1:1;
ex d1 being Element of F₁() ex d2 being Element of F₂() st d = [d1,d2] by DOMAIN_1:1;
hence P₁[d,d9] by A1, A2; :: thesis: verum