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

P₁[F₂()]

provided

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