scheme :: FRAENKEL:sch 9
RelevantArgs{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> Function of F₁(),F₂(), F₅() -> Function of F₁(),F₂(), P₁[ object ], P₂[ object ] } :

{ (F₄() . u9) where u9 is Element of F₁() : ( P₁[u9] & u9 in F₃() ) } = { (F₅() . v9) where v9 is Element of F₁() : ( P₂[v9] & v9 in F₃() ) }

provided

A1: F₄() | F₃() = F₅() | F₃() and
A2: for u being Element of F₁() st u in F₃() holds
( P₁[u] iff P₂[u] )