defpred S_{1}[ set , set ] means ( $2 = F_{4}() & P_{1}[$1,$2] );

A1: for s being Element of F_{1}()

for t being Element of F_{2}() holds

( S_{1}[s,t] iff ( t = F_{4}() & P_{1}[s,t] ) )
;

thus { F_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : S_{1}[s,t] } = { F_{3}(s9,F_{4}()) where s9 is Element of F_{1}() : P_{1}[s9,F_{4}()] }
from FRAENKEL:sch 19(A1); :: thesis: verum

A1: for s being Element of F

for t being Element of F

( S

thus { F