scheme :: FRAENKEL:sch 12
Gen199A{ F₁() -> set , F₂() -> set , F₃( object , object ) -> object , P₁[ object , object ], P₂[ object ] } :

for st1 being set st st1 in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₁[s1,t1] } holds
P₂[st1]

provided

A1: for s being Element of F₁()
for t being Element of F₂() st P₁[s,t] holds
P₂[F₃(s,t)]