set Y = the V3() 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 V3() ManySortedSet of the carrier of S = the carrier of S ) by PARTFUN1:def 2;

then A4: (dom the V3() ManySortedSet of the carrier of S) \/ (dom X) = the carrier of S by A1, XBOOLE_1:12, INSTALG1:10;

then dom ( the V3() ManySortedSet of the carrier of S +* X) = the carrier of S by FUNCT_4:def 1;

then reconsider YX = the V3() 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 V3()_{1} being V3() ManySortedSet of the carrier of S st b_{1} is X -tolerating
; :: thesis: verum

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 V3() ManySortedSet of the carrier of S = the carrier of S ) by PARTFUN1:def 2;

then A4: (dom the V3() ManySortedSet of the carrier of S) \/ (dom X) = the carrier of S by A1, XBOOLE_1:12, INSTALG1:10;

then dom ( the V3() ManySortedSet of the carrier of S +* X) = the carrier of S by FUNCT_4:def 1;

then reconsider YX = the V3() 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 V3()

proof

hence
ex b
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;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