defpred S₁[ set , set ] means ( P₂[$1] & P₁[$1,$2] );
defpred S₂[ set , set ] means ( $1 in { s1 where s1 is Element of F₁() : P₂[s1] } & P₁[$1,$2] );
A1: for s being Element of F₁()
for t being Element of F₂() holds
( S₂[s,t] iff S₁[s,t] )

proof

let s be Element of F₁(); :: thesis: for t being Element of F₂() holds
( S₂[s,t] iff S₁[s,t] )
let t be Element of F₂(); :: thesis: ( S₂[s,t] iff S₁[s,t] )

now :: thesis: ( s in { s1 where s1 is Element of F₁() : P₂[s1] } implies P₂[s] )

assume s in { s1 where s1 is Element of F₁() : P₂[s1] } ; :: thesis: P₂[s]
then ex s1 being Element of F₁() st
( s = s1 & P₂[s1] ) ;
hence P₂[s] ; :: thesis: verum

end;

hence ( S₂[s,t] iff S₁[s,t] ) ; :: thesis: verum

end;

thus { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : S₂[s,t] } = { F₃(s2,t2) where s2 is Element of F₁(), t2 is Element of F₂() : S₁[s2,t2] } from FRAENKEL:sch 4(A1); :: thesis: verum