defpred S1[ object , object , object ] means ( P1[\$1,\$2] & \$3 = F4(\$1,\$2) );
A2: for x, y, z1, z2 being object st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2 ;
A3: for x, y, z being object st x in F1() & y in F2() & S1[x,y,z] holds
z in F3() by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A4: for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being object st S1[x,y,z] ) ) and
A5: for x, y being object st [x,y] in dom f holds
S1[x,y,f . (x,y)] from take f ; :: thesis: ( ( for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )

thus for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) :: thesis: for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y)
proof
let x, y be object ; :: thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) )
thus ( [x,y] in dom f implies ( x in F1() & y in F2() & P1[x,y] ) ) :: thesis: ( x in F1() & y in F2() & P1[x,y] implies [x,y] in dom f )
proof
assume A6: [x,y] in dom f ; :: thesis: ( x in F1() & y in F2() & P1[x,y] )
then ex z being object st
( P1[x,y] & z = F4(x,y) ) by A4;
hence ( x in F1() & y in F2() & P1[x,y] ) by A4, A6; :: thesis: verum
end;
assume that
A7: ( x in F1() & y in F2() ) and
A8: P1[x,y] ; :: thesis: [x,y] in dom f
ex z being object st
( P1[x,y] & z = F4(x,y) ) by A8;
hence [x,y] in dom f by A4, A7; :: thesis: verum
end;
thus for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y) by A5; :: thesis: verum