set Y = the empty-yielding ManySortedSet of the carrier of S;
A1: J is Subsignature of S by Def2;
then A2: the carrier of J c= the carrier of S by INSTALG1:10;
A3: ( dom X = the carrier of J & dom the empty-yielding ManySortedSet of the carrier of S = the carrier of S ) by PARTFUN1:def 2;
then A4: (dom the empty-yielding ManySortedSet of the carrier of S) \/ (dom X) = the carrier of S by A1, XBOOLE_1:12, INSTALG1:10;
then dom ( the empty-yielding ManySortedSet of the carrier of S +* X) = the carrier of S by FUNCT_4:def 1;
then reconsider YX = the empty-yielding ManySortedSet of the carrier of S +* X as ManySortedSet of the carrier of S by RELAT_1:def 18, PARTFUN1:def 2;
consider a being object such that
A5: ( a in the carrier of J & not X . a is empty ) by PBOOLE:def 12;
YX is empty-yielding

proof

take a ; :: according to PBOOLE:def 12 :: thesis: ( a in the carrier of S & not YX . a is empty )
thus a in the carrier of S by A2, A5; :: thesis: not YX . a is empty
thus not YX . a is empty by A2, A3, A5, A4, FUNCT_4:def 1; :: thesis: verum

end;

hence ex b₁ being empty-yielding ManySortedSet of the carrier of S st b₁ is X -tolerating ; :: thesis: verum