defpred S₁[ set , set ] 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₂[ set ] 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 set holds
( z in T iff ( z in [:F₁(),F₂():] & S₂[z] ) ) from XBOOLE_0:sch 1();
A3: for x1 being set st x1 in T holds
ex z being set st S₁[x1,z]

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

per cases by A2, A4, A7;

suppose A8: P₁[q',w'] ; :: thesis:

take z = F₄(q',w'); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q' = c & w' = d ) by A7, ZFMISC_1:33;
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₂[q',w'] ; :: thesis:

take z = F₅(q',w'); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q' = c & w' = d ) by A7, ZFMISC_1:33;
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₃[q',w'] ; :: thesis:

take z = F₆(q',w'); :: thesis:
let c be Element of F₁(); :: thesis:
let d be Element of F₂(); :: thesis:
assume x1 = [c,d] ; :: thesis:
then ( q' = c & w' = d ) by A7, ZFMISC_1:33;
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 set st S₁[x1,z] ; :: thesis:

end;

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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng f ; :: thesis:
then consider x1 being set such that
A13: x1 in dom f and
A14: z = f . x1 by FUNCT_1:def 5;
x1 in [:F₁(),F₂():] by A2, A11, A13;
then consider x, y being set 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

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₂():]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in T ; :: thesis:
hence z in [:F₁(),F₂():] by A2; :: thesis:

end;

then reconsider f = f as PartFunc of , by A11, A12, RELSET_1:11;
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

let i' be Element of F₁(); :: thesis:
let o' be Element of F₂(); :: thesis:
assume A20: [c,d] = [i',o'] ; :: thesis:
then c = i' by ZFMISC_1:33;
hence ( P₁[i',o'] or P₂[i',o'] or P₃[i',o'] ) by A18, A20, ZFMISC_1:33; :: thesis:

end;

[c,d] in [:F₁(),F₂():] by ZFMISC_1:106;
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: