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