rng p c= I ;
then rng p c= dom X by PARTFUN1:def 2;
then dom (X * p) = dom p by RELAT_1:27;
then reconsider Xp = X * p as ManySortedSet of dom p by PARTFUN1:def 2;
Xp is ManySortedSet of dom p ;
hence for b₁ being dom p -defined Function st b₁ = X * p holds
b₁ is total ; :: thesis: verum