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

{ F₅(u,v) where u is Element of F₁(), v is Element of F₂() : ( u in F₃() & v in F₄() ) } is finite

provided

A1: F₃() is finite and
A2: F₄() is finite