consider x being object such that

A1: ( x in the carrier of J & not X . x is empty ) by PBOOLE:def 12;

take x ; :: according to PBOOLE:def 12 :: thesis: ( x in the carrier of S & not (X extended_by (Y, 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 (Y, the carrier of S)) . x is empty

dom X = the carrier of J by PARTFUN1:def 2;

then x in dom (X | the carrier of S) by A1, A2, RELAT_1:57;

then (X extended_by (Y, 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 (Y, the carrier of S)) . x is empty by A1; :: thesis: verum

A1: ( x in the carrier of J & not X . x is empty ) by PBOOLE:def 12;

take x ; :: according to PBOOLE:def 12 :: thesis: ( x in the carrier of S & not (X extended_by (Y, 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 (Y, the carrier of S)) . x is empty

dom X = the carrier of J by PARTFUN1:def 2;

then x in dom (X | the carrier of S) by A1, A2, RELAT_1:57;

then (X extended_by (Y, 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 (Y, the carrier of S)) . x is empty by A1; :: thesis: verum