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

{ F₂(v1) where v1 is Element of F₁() : P₁[v1] } = { F₃(v2) where v2 is Element of F₁() : P₁[v2] }

provided

A1: for v being Element of F₁() st P₁[v] holds
F₂(v) = F₃(v)