> ⊢ ∀x[1]∈S[1] ... ∀x[k]∈S[k] ( A(x[1],...,x[k]) ⇔ Q(x[1],...,x[k]) ). [where Q is a k-parameter property and A is a fresh predicate-symbol]
> ∀x[1]∈S[1] ... ∀x[k]∈S[k] ∃!y∈T ( Q(x[1],...,x[k],y) ) ⊢ ∀x[1]∈S[1] ... ∀x[k]∈S[k] ( f(x[1],...,x[k])∈T ∧ Q(x[1],...,x[k],f(x[1],...,x[k])) ). [where Q is a (k+1)-parameter property and f is a fresh function-symbol]