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, RELAT_1:def 18;
Xp is ManySortedSet of dom p ;
hence for b₁ being Function st b₁ = X * p holds
b₁ is dom p -defined ; :: thesis: verum