rng p c= I ;
then rng p c= dom X by PBOOLE:def 3;
then dom (X * p) = dom p by RELAT_1:46;
then reconsider Xp = X * p as ManySortedSet of dom p by PBOOLE:def 3;
Xp is ManySortedSet of dom p ;
hence p * X is ManySortedSet of dom p ; :: thesis: verum