defpred S1[ set , set ] means P1[$1,$2];
A1: for c being Element of F1()
for f being Element of F2() st P1[c,f] holds
not S1[c,f] ;
consider f being PartFunc of [:F1(),F2():],F3() such that
A2: ( ( for c being Element of F1()
for e being Element of F2() holds
( [c,e] in dom f iff ( P1[c,e] or S1[c,e] ) ) ) & ( for c being Element of F1()
for g being Element of F2() st [c,g] in dom f holds
( ( P1[c,g] implies f . [c,g] = F4(c,g) ) & ( S1[c,g] implies f . [c,g] = F5(c,g) ) ) ) ) from SCHEME1:sch 15(A1);
 consider g being Function such that
A3: g = 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
A4: y in F1() and
A5: z in F2() and
A6: x = [y,z] by ZFMISC_1:def 2;
reconsider z = z as Element of F2() by A5;
reconsider y = y as Element of F1() by A4;
( P1[y,z] or not P1[y,z] ) ;
hence x in dom f by A2, A6; :: thesis: verum
end;
then reconsider g = g as Function of [:F1(),F2():],F3() by A3, FUNCT_2:def 1;
take g ; :: thesis: for c being Element of F1()
for d being Element of F2() st [c,d] in dom g holds
( ( P1[c,d] implies g . [c,d] = F4(c,d) ) & ( P1[c,d] implies g . [c,d] = F5(c,d) ) )
thus for c being Element of F1()
for d being Element of F2() st [c,d] in dom g holds
( ( P1[c,d] implies g . [c,d] = F4(c,d) ) & ( P1[c,d] implies g . [c,d] = F5(c,d) ) ) by A2, A3; :: thesis: verum