scheme :: FRAENKEL:sch 25
ImFin{ F₁() -> set , F₂() -> non empty set , F₃() -> set , F₄() -> set , F₅( object ) -> object } :

{ F₅(phi9) where phi9 is Element of Funcs (F₁(),F₂()) : phi9 .: F₃() c= F₄() } is finite

provided

A1: F₃() is finite and
A2: F₄() is finite and
A3: for phi, psi being Element of Funcs (F₁(),F₂()) st phi | F₃() = psi | F₃() holds
F₅(phi) = F₅(psi)