let S be OrderSortedSign; :: thesis: for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff Name op1 = Name op2 )
let op1, op2 be OperSymbol of S; :: thesis: ( op1 ~= op2 iff Name op1 = Name op2 )
( op2 in Class ( the Overloading of S,op1) iff Class ( the Overloading of S,op1) = Class ( the Overloading of S,op2) ) by EQREL_1:23;
hence ( op1 ~= op2 iff Name op1 = Name op2 ) by Th30; :: thesis: verum