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

defpred S_{2}[ set , set ] means ( $1 in { s1 where s1 is Element of F_{1}() : P_{2}[s1] } & P_{1}[$1,$2] );

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

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

( S_{2}[s,t] iff S_{1}[s,t] )
_{3}(s,t) where s is Element of F_{1}(), t is Element of F_{2}() : S_{2}[s,t] } = { F_{3}(s2,t2) where s2 is Element of F_{1}(), t2 is Element of F_{2}() : S_{1}[s2,t2] }
from FRAENKEL:sch 4(A1); :: thesis: verum

defpred S

A1: for s being Element of F

for t being Element of F

( S

proof

thus
{ F
let s be Element of F_{1}(); :: thesis: for t being Element of F_{2}() holds

( S_{2}[s,t] iff S_{1}[s,t] )

let t be Element of F_{2}(); :: thesis: ( S_{2}[s,t] iff S_{1}[s,t] )

_{2}[s,t] iff S_{1}[s,t] )
; :: thesis: verum

end;( S

let t be Element of F

now :: thesis: ( s in { s1 where s1 is Element of F_{1}() : P_{2}[s1] } implies P_{2}[s] )

hence
( Sassume
s in { s1 where s1 is Element of F_{1}() : P_{2}[s1] }
; :: thesis: P_{2}[s]

then ex s1 being Element of F_{1}() st

( s = s1 & P_{2}[s1] )
;

hence P_{2}[s]
; :: thesis: verum

end;then ex s1 being Element of F

( s = s1 & P

hence P