defpred S₁[ object , object ] means for c being Element of F₁()
for t being Element of F₂() st $1 = [c,t] holds
( ( P₁[c,t] implies $2 = F₄(c,t) ) & ( P₂[c,t] implies $2 = F₅(c,t) ) & ( P₃[c,t] implies $2 = F₆(c,t) ) );
defpred S₂[ object ] means for c being Element of F₁()
for d being Element of F₂() holds
( not $1 = [c,d] or P₁[c,d] or P₂[c,d] or P₃[c,d] );
consider T being set such that
A2: for z being object holds
( z in T iff ( z in [:F₁(),F₂():] & S₂[z] ) ) from XBOOLE_0:sch 1();
A3: for x1 being object st x1 in T holds
ex z being object st S₁[x1,z]

let x1 be object ; :: thesis:
assume A4: x1 in T ; :: thesis:
then x1 in [:F₁(),F₂():] by A2;
then consider q9, w9 being object such that
A5: q9 in F₁() and
A6: w9 in F₂() and
A7: x1 = [q9,w9] by ZFMISC_1:def 2;
reconsider w9 = w9 as Element of F₂() by A6;
reconsider q9 = q9 as Element of F₁() by A5;

per cases by A2, A4, A7;

suppose A8: P₁[q9,w9] ; :: thesis:

take z = F₄(q9,w9); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;
hence ( ( P₁[c,d] implies z = F₄(c,d) ) & ( P₂[c,d] implies z = F₅(c,d) ) & ( P₃[c,d] implies z = F₆(c,d) ) ) by A1, A8; :: thesis:

end;

suppose A9: P₂[q9,w9] ; :: thesis:

take z = F₅(q9,w9); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;
hence ( ( P₁[c,d] implies z = F₄(c,d) ) & ( P₂[c,d] implies z = F₅(c,d) ) & ( P₃[c,d] implies z = F₆(c,d) ) ) by A1, A9; :: thesis:

end;

suppose A10: P₃[q9,w9] ; :: thesis:

take z = F₆(q9,w9); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1;
hence ( ( P₁[c,d] implies z = F₄(c,d) ) & ( P₂[c,d] implies z = F₅(c,d) ) & ( P₃[c,d] implies z = F₆(c,d) ) ) by A1, A10; :: thesis:

end;

hence ex z being object st S₁[x1,z] ; :: thesis:

end;

consider f being Function such that
A11: ( dom f = T & ( for z being object st z in T holds
S₁[z,f . z] ) ) from CLASSES1:sch 1(A3);
A12: rng f c= F₃()

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng f ; :: thesis:
then consider x1 being object such that
A13: x1 in dom f and
A14: z = f . x1 by FUNCT_1:def 3;
x1 in [:F₁(),F₂():] by A2, A11, A13;
then consider x, y being object such that
A15: x in F₁() and
A16: y in F₂() and
A17: x1 = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Element of F₂() by A16;
reconsider x = x as Element of F₁() by A15;

now :: thesis:

per cases by A2, A11, A13, A17;

suppose P₁[x,y] ; :: thesis:

then f . [x,y] = F₄(x,y) by A11, A13, A17;
hence z in F₃() by A14, A17; :: thesis:

end;

suppose P₂[x,y] ; :: thesis:

then f . [x,y] = F₅(x,y) by A11, A13, A17;
hence z in F₃() by A14, A17; :: thesis:

end;

suppose P₃[x,y] ; :: thesis:

then f . [x,y] = F₆(x,y) by A11, A13, A17;
hence z in F₃() by A14, A17; :: thesis:

end;

hence z in F₃() ; :: thesis:

end;

T c= [:F₁(),F₂():] by A2;
then reconsider f = f as PartFunc of [:F₁(),F₂():],F₃() by A11, A12, RELSET_1:4;
take f ; :: thesis:
thus for c being Element of F₁()
for d being Element of F₂() holds
( [c,d] in dom f iff ( P₁[c,d] or P₂[c,d] or P₃[c,d] ) ) :: thesis:

proof

let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
thus ( not [c,d] in dom f or P₁[c,d] or P₂[c,d] or P₃[c,d] ) by A2, A11; :: thesis:
assume A18: ( P₁[c,d] or P₂[c,d] or P₃[c,d] ) ; :: thesis:

A19: now :: thesis:

let i9 be Element of F₁(); :: thesis:
let o9 be Element of F₂(); :: thesis:
assume A20: [c,d] = [i9,o9] ; :: thesis:
then c = i9 by XTUPLE_0:1;
hence ( P₁[i9,o9] or P₂[i9,o9] or P₃[i9,o9] ) by A18, A20, XTUPLE_0:1; :: thesis:

end;

[c,d] in [:F₁(),F₂():] by ZFMISC_1:87;
hence [c,d] in dom f by A2, A11, A19; :: thesis:

end;

let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume [c,d] in dom f ; :: thesis:
hence ( ( P₁[c,d] implies f . [c,d] = F₄(c,d) ) & ( P₂[c,d] implies f . [c,d] = F₅(c,d) ) & ( P₃[c,d] implies f . [c,d] = F₆(c,d) ) ) by A11; :: thesis: