let S be OrderSortedSign; :: thesis: for on being OperName of S
for op being OperSymbol of S holds
( op is Element of on iff Name op = on )
let on be OperName of S; :: thesis: for op being OperSymbol of S holds
( op is Element of on iff Name op = on )
let op1 be OperSymbol of S; :: thesis: ( op1 is Element of on iff Name op1 = on )

hereby :: thesis: ( Name op1 = on implies op1 is Element of on )

assume op1 is Element of on ; :: thesis: Name op1 = on
then reconsider op = op1 as Element of on ;
( ex op2 being object st
( op2 in the carrier' of S & on = Class ( the Overloading of S,op2) ) & Name op = Class ( the Overloading of S,op) ) by EQREL_1:def 3;
hence Name op1 = on by EQREL_1:23; :: thesis: verum

end;

assume Name op1 = on ; :: thesis: op1 is Element of on
hence op1 is Element of on by EQREL_1:20; :: thesis: verum