let st1 be set ; :: thesis: ( st1 in { F_{3}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] } implies P_{2}[st1] )

assume st1 in { F_{3}(s1,t1) where s1 is Element of F_{1}(), t1 is Element of F_{2}() : P_{1}[s1,t1] }
; :: thesis: P_{2}[st1]

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

( st1 = F_{3}(s1,t1) & P_{1}[s1,t1] )
;

hence P_{2}[st1]
by A1; :: thesis: verum

assume st1 in { F

then ex s1 being Element of F

( st1 = F

hence P