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

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