defpred S1[ set , set ] means ( $2 = F4() & P1[$1,$2] );
A1:
for s being Element of F1()
for t being Element of F2() holds
( S1[s,t] iff ( t = F4() & P1[s,t] ) )
;
thus
{ F3(s,t) where s is Element of F1(), t is Element of F2() : S1[s,t] } = { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }
from FRAENKEL:sch 19(A1); verum