dom (J --> y) = J by FUNCOP_1:19;
hence J => y is ManySortedSet of J ; :: thesis: verum