dom (id X) = X ;
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:58, XBOOLE_1:12;
hence (id X) +* (f | X) is ManySortedSet of X by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum