defpred S1[ set ] means for c being Element of F1()
for d being Element of F2() holds
( not $1 = [c,d] or P1[c,d] or P2[c,d] );
consider F being set such that
A2: for z being set holds
( z in F iff ( z in [:F1(),F2():] & S1[z] ) ) from XBOOLE_0:sch 1();
 A3: F c= [:F1(),F2():]
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in F or z in [:F1(),F2():] )
assume z in F ; :: thesis: z in [:F1(),F2():]
hence z in [:F1(),F2():] by A2; :: thesis: verum
end;
defpred S2[ set , set ] means for c being Element of F1()
for t being Element of F2() st $1 = [c,t] holds
( ( P1[c,t] implies $2 = F4(c,t) ) & ( P2[c,t] implies $2 = F5(c,t) ) );
A4: for x1 being set st x1 in F holds
ex z being set st S2[x1,z]
proof
let x1 be set ; :: thesis: ( x1 in F implies ex z being set st S2[x1,z] )
assume A5: x1 in F ; :: thesis: ex z being set st S2[x1,z]
then x1 in [:F1(),F2():] by A2;
then consider f', g' being set such that
A6: ( f' in F1() & g' in F2() & x1 = [f',g'] ) by ZFMISC_1:def 2;
reconsider f' = f' as Element of F1() by A6;
reconsider g' = g' as Element of F2() by A6;
now
per cases ( P1[f',g'] or P2[f',g'] ) by A2, A5, A6;
suppose A7: P1[f',g'] ; :: thesis: ex z being Element of F3() st
for p being Element of F1()
for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
take z = F4(f',g'); :: thesis: for p being Element of F1()
for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
let p be Element of F1(); :: thesis: for d being Element of F2() st x1 = [p,d] holds
( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
let d be Element of F2(); :: thesis: ( x1 = [p,d] implies ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) )
assume x1 = [p,d] ; :: thesis: ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) )
then ( f' = p & g' = d ) by A6, ZFMISC_1:33;
hence ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) by A1, A7; :: thesis: verum
end;
suppose A8: P2[f',g'] ; :: thesis: ex z being Element of F3() st
for r being Element of F1()
for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
take z = F5(f',g'); :: thesis: for r being Element of F1()
for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
let r be Element of F1(); :: thesis: for d being Element of F2() st x1 = [r,d] holds
( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
let d be Element of F2(); :: thesis: ( x1 = [r,d] implies ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) )
assume x1 = [r,d] ; :: thesis: ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) )
then ( f' = r & g' = d ) by A6, ZFMISC_1:33;
hence ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) by A1, A8; :: thesis: verum
end;
end;
end;
hence ex z being set st S2[x1,z] ; :: thesis: verum
end;
consider f being Function such that
A9: ( dom f = F & ( for z being set st z in F holds
S2[z,f . z] ) ) from CLASSES1:sch 1(A4);
 rng f c= F3()
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in F3() )
assume z in rng f ; :: thesis: z in F3()
then consider x1 being set such that
A10: ( x1 in dom f & z = f . x1 ) by FUNCT_1:def 5;
x1 in [:F1(),F2():] by A2, A9, A10;
then consider x, y being set such that
A11: ( x in F1() & y in F2() & x1 = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x as Element of F1() by A11;
reconsider y = y as Element of F2() by A11;
now
end;
hence z in F3() ; :: thesis: verum
end;
then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A3, A9, RELSET_1:11;
take f ; :: thesis: ( ( for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom f iff ( P1[c,d] or P2[c,d] ) ) ) & ( for c being Element of F1()
for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) )
thus for c being Element of F1()
for h being Element of F2() holds
( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) ) :: thesis: for c being Element of F1()
for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
proof
let c be Element of F1(); :: thesis: for h being Element of F2() holds
( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) )
let g be Element of F2(); :: thesis: ( [c,g] in dom f iff ( P1[c,g] or P2[c,g] ) )
thus ( not [c,g] in dom f or P1[c,g] or P2[c,g] ) by A2, A9; :: thesis: ( ( P1[c,g] or P2[c,g] ) implies [c,g] in dom f )
assume A12: ( P1[c,g] or P2[c,g] ) ; :: thesis: [c,g] in dom f
A13: [c,g] in [:F1(),F2():] by ZFMISC_1:106;
now
let h' be Element of F1(); :: thesis: for j' being Element of F2() holds
( not [c,g] = [h',j'] or P1[h',j'] or P2[h',j'] )
let j' be Element of F2(); :: thesis: ( not [c,g] = [h',j'] or P1[h',j'] or P2[h',j'] )
assume [c,g] = [h',j'] ; :: thesis: ( P1[h',j'] or P2[h',j'] )
then ( c = h' & g = j' ) by ZFMISC_1:33;
hence ( P1[h',j'] or P2[h',j'] ) by A12; :: thesis: verum
end;
hence [c,g] in dom f by A2, A9, A13; :: thesis: verum
end;
let c be Element of F1(); :: thesis: for d being Element of F2() st [c,d] in dom f holds
( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
let d be Element of F2(); :: thesis: ( [c,d] in dom f implies ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) )
assume [c,d] in dom f ; :: thesis: ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) )
hence ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) by A9; :: thesis: verum