scheme :: WAYBEL24:sch 3
FraenkelF9RS{ F₁() -> non empty TopRelStr , F₂( set ) -> set , F₃( set ) -> set , P₁[ set ] } :

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