let S0 be non empty non void ManySortedSign ; :: thesis: ( OSSign S0 is discrete & OSSign S0 is op-discrete )
set s = OSSign S0;
set ol = the Overloading of (OSSign S0);
( the carrier of S0 = the carrier of (OSSign S0) & id the carrier of S0 = the InternalRel of (OSSign S0) ) by Def6;
hence OSSign S0 is discrete by ORDERS_3:def 1; :: thesis: OSSign S0 is op-discrete
A1: the Overloading of (OSSign S0) = id the carrier' of S0 by Def6;

now

let x, y be OperSymbol of (OSSign S0); :: thesis: ( x ~= y implies x = y )
assume x ~= y ; :: thesis: x = y
then [x,y] in the Overloading of (OSSign S0) by Def3;
hence x = y by A1, RELAT_1:def 10; :: thesis: verum

end;

hence OSSign S0 is op-discrete by Th3; :: thesis: verum