defpred S₁[ set , set ] means P₁[$1,$2];
A1: for c being Element of F₁()
for f being Element of F₂() st P₁[c,f] holds
not S₁[c,f] ;
consider f being PartFunc of [:F₁(),F₂():],F₃() such that
A2: ( ( for c being Element of F₁()
for e being Element of F₂() holds
( [c,e] in dom f iff ( P₁[c,e] or S₁[c,e] ) ) ) & ( for c being Element of F₁()
for g being Element of F₂() st [c,g] in dom f holds
( ( P₁[c,g] implies f . [c,g] = F₄(c,g) ) & ( S₁[c,g] implies f . [c,g] = F₅(c,g) ) ) ) ) from SCHEME1:sch 15(A1);
consider g being Function such that
A3: g = f ;
dom f = [:F₁(),F₂():]

proof

thus dom f c= [:F₁(),F₂():] ; :: according to XBOOLE_0:def 10 :: thesis: [:F₁(),F₂():] c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:F₁(),F₂():] or x in dom f )
assume x in [:F₁(),F₂():] ; :: thesis: x in dom f
then consider y, z being object such that
A4: y in F₁() and
A5: z in F₂() and
A6: x = [y,z] by ZFMISC_1:def 2;
reconsider z = z as Element of F₂() by A5;
reconsider y = y as Element of F₁() by A4;
( P₁[y,z] or not P₁[y,z] ) ;
hence x in dom f by A2, A6; :: thesis: verum

end;

then reconsider g = g as Function of [:F₁(),F₂():],F₃() by A3, FUNCT_2:def 1;
take g ; :: thesis: for c being Element of F₁()
for d being Element of F₂() st [c,d] in dom g holds
( ( P₁[c,d] implies g . [c,d] = F₄(c,d) ) & ( P₁[c,d] implies g . [c,d] = F₅(c,d) ) )
thus for c being Element of F₁()
for d being Element of F₂() st [c,d] in dom g holds
( ( P₁[c,d] implies g . [c,d] = F₄(c,d) ) & ( P₁[c,d] implies g . [c,d] = F₅(c,d) ) ) by A2, A3; :: thesis: verum