dom (id X) = X by RELAT_1:71;
then ( dom ((id X) +* (f | X)) = X \/ (dom (f | X)) & dom (f | X) c= X ) by FUNCT_4:def 1, RELAT_1:87;
then dom ((id X) +* (f | X)) = X by XBOOLE_1:12;
hence (id X) +* (f | X) is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum