let S be non empty non void OverloadedMSSign ; :: thesis: ( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds
x = y )
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: ( ( for x, y being OperSymbol of S st x ~= y holds
x = y ) implies S is op-discrete )
assume A1: for x, y being OperSymbol of S st x ~= y holds
x = y ; :: thesis: S is op-discrete

now :: thesis: for x, y being object holds
( ( [x,y] in the Overloading of S implies ( x in the carrier' of S & x = y ) ) & ( x in the carrier' of S & x = y implies [x,y] in the Overloading of S ) )

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

proof

assume A2: [x,y] in the Overloading of S ; :: thesis: ( x in the carrier' of S & x = y )
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: verum

end;

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

end;

hence the Overloading of S = id the carrier' of S by RELAT_1:def 10; :: according to OSALG_1:def 4 :: thesis: verum