scheme :: FRAENKEL:sch 21
FraenkelFin{ F₁() -> set , F₂() -> set , F₃( object ) -> object } :

{ F₃(w) where w is Element of F₁() : w in F₂() } is finite

provided

A1: F₂() is finite