let S be non empty non void OverloadedMSSign ; :: thesis:
set d = id the carrier' of S;
set opss = the carrier' of S;
set ol = the Overloading of S;
thus ( S is op-discrete implies for x, y being OperSymbol of S st x ~= y holds
x = y ) by RELAT_1:def 10; :: thesis:
assume A1: for x, y being OperSymbol of S st x ~= y holds
x = y ; :: thesis:

let x, y be object ; :: thesis:
thus ( [x,y] in the Overloading of S implies ( x in the carrier' of S & x = y ) ) :: thesis:

assume A2: [x,y] in the Overloading of S ; :: thesis:
then ex x1, y1 being object st
( [x,y] = [x1,y1] & x1 in the carrier' of S & y1 in the carrier' of S ) by RELSET_1:2;
then reconsider x2 = x, y2 = y as OperSymbol of S by XTUPLE_0:1;
x2 ~= y2 by A2;
hence ( x in the carrier' of S & x = y ) by A1; :: thesis:

end;

assume ( x in the carrier' of S & x = y ) ; :: thesis:
hence [x,y] in the Overloading of S by Def2; :: thesis:

end;