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

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

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