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

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

provided

A1: F₁() c= F₂() and
A2: for d1, d2 being Element of F₂() st d1 in F₁() & d2 in F₁() & F₃(d1) = F₃(d2) holds
d1 = d2