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 PARTFUN1:def 2; :: thesis: verum