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:31;
hence ( op1 ~= op2 iff Name op1 = Name op2 ) by Th30; :: thesis: verum