defpred S₁[ set , set ] means ( $2 = F₄() & P₁[$1,$2] );
A1: for s being Element of F₁()
for t being Element of F₂() holds
( S₁[s,t] iff ( t = F₄() & P₁[s,t] ) ) ;
thus { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : S₁[s,t] } = { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } from FRAENKEL:sch 19(A1); :: thesis: verum