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 Def5;
hence OSSign S0 is discrete by ORDERS_3:def 1; :: thesis: OSSign S0 is op-discrete
the Overloading of (OSSign S0) = id the carrier' of S0 by Def5;
then for x, y being OperSymbol of (OSSign S0) st x ~= y holds
x = y by RELAT_1:def 10;
hence OSSign S0 is op-discrete by Th3; :: thesis: verum