{ 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] }

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) )