A3: for c being Element of F1()
for d being Element of F2() holds
( ( P1[c,d] implies not P2[c,d] ) & ( P1[c,d] implies not P3[c,d] ) & ( P2[c,d] implies not P3[c,d] ) ) by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A4: ( ( for c being Element of F1()
for b being Element of F2() holds
( [c,b] in dom f iff ( P1[c,b] or P2[c,b] or P3[c,b] ) ) ) & ( for a being Element of F1()
for b being Element of F2() st [a,b] in dom f holds
( ( P1[a,b] implies f . [a,b] = F4(a,b) ) & ( P2[a,b] implies f . [a,b] = F5(a,b) ) & ( P3[a,b] implies f . [a,b] = F6(a,b) ) ) ) ) from SCHEME1:sch 16(A3);
 consider v being Function such that
A5: v = f ;
dom f = [:F1(),F2():]
proof
thus dom f c= [:F1(),F2():] ; :: according to XBOOLE_0:def 10 :: thesis: [:F1(),F2():] c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:F1(),F2():] or x in dom f )
assume x in [:F1(),F2():] ; :: thesis: x in dom f
then consider y, z being object such that
A6: y in F1() and
A7: z in F2() and
A8: x = [y,z] by ZFMISC_1:def 2;
reconsider z = z as Element of F2() by A7;
reconsider y = y as Element of F1() by A6;
( P1[y,z] or P2[y,z] or P3[y,z] ) by A2;
hence x in dom f by A4, A8; :: thesis: verum
end;
then reconsider v = v as Function of [:F1(),F2():],F3() by A5, FUNCT_2:def 1;
take v ; :: thesis: ( ( for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom v iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1()
for d being Element of F2() st [c,d] in dom v holds
( ( P1[c,d] implies v . [c,d] = F4(c,d) ) & ( P2[c,d] implies v . [c,d] = F5(c,d) ) & ( P3[c,d] implies v . [c,d] = F6(c,d) ) ) ) )
thus ( ( for c being Element of F1()
for d being Element of F2() holds
( [c,d] in dom v iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1()
for d being Element of F2() st [c,d] in dom v holds
( ( P1[c,d] implies v . [c,d] = F4(c,d) ) & ( P2[c,d] implies v . [c,d] = F5(c,d) ) & ( P3[c,d] implies v . [c,d] = F6(c,d) ) ) ) ) by A4, A5; :: thesis: verum