scheme :: FRAENKEL:sch 19
FrEqua1{ F₁() -> set , F₂() -> set , F₃( object , object ) -> object , F₄() -> Element of F₂(), P₁[ object , object ], P₂[ object , object ] } :

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

provided

A1: for s being Element of F₁()
for t being Element of F₂() holds
( P₂[s,t] iff ( t = F₄() & P₁[s,t] ) )