scheme :: FUNCT_7:sch 3
CardMono{ F₁() -> set , F₂() -> non empty set , F₃( object ) -> object } :

F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

provided

A1: for x being set st x in F₁() holds
ex d being Element of F₂() st x = F₃(d) and
A2: for d1, d2 being Element of F₂() st F₃(d1) = F₃(d2) holds
d1 = d2