set f = I --> A;
dom (I --> A) = I by FUNCOP_1:19;
hence I --> A is ManySortedSet of I by PBOOLE:def 3; :: thesis: verum