set Y = X extended_by ({}, the carrier of S);
consider x being object such that
A1: ( x in the carrier of J & not X . x is empty ) by PBOOLE:def 12;
X extended_by ({}, the carrier of S) is V3()
proof
take x ; :: according to PBOOLE:def 12 :: thesis: ( x in the carrier of S & not (X extended_by ({}, the carrier of S)) . x is empty )
J is Subsignature of S by Def2;
then A2: the carrier of J c= the carrier of S by INSTALG1:10;
hence x in the carrier of S by A1; :: thesis: not (X extended_by ({}, the carrier of S)) . x is empty
x in dom X by A1, PARTFUN1:def 2;
then x in dom (X | the carrier of S) by A2, RELAT_1:57;
then (X extended_by ({}, the carrier of S)) . x = (X | the carrier of S) . x by FUNCT_4:13
.= X . x by A1, A2, FUNCT_1:49 ;
hence not (X extended_by ({}, the carrier of S)) . x is empty by A1; :: thesis: verum
end;
hence ex b1 being V3() ManySortedSet of the carrier of S st b1 is X -tolerating ; :: thesis: verum