scheme :: LMOD_7:sch 8
Fr2{ F₁() -> set , F₂() -> non empty set , F₃() -> Element of F₂(), P₁[ object ] } :

P₁[F₃()]

provided

A1: F₃() in F₁() and
A2: F₁() = { a where a is Element of F₂() : P₁[a] }