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

{ F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₁[s,t] } c= { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₂[s1,t1] }

provided

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