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