let st1 be set ; ( st1 in { F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1] } implies P2[st1] )
assume
st1 in { F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1] }
; P2[st1]
then
ex s1 being Element of F1() ex t1 being Element of F2() st
( st1 = F3(s1,t1) & P1[s1,t1] )
;
hence
P2[st1]
by A1; verum