the carrier of R = dom (the carrier of R --> z) by FUNCT_2:def 1;
hence the carrier of R --> z is ManySortedSet of the carrier of R by PBOOLE:def 3; :: thesis: verum