let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2
let o1, o2 be OperSymbol of S; :: thesis: ( S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} implies o1 = o2 )
assume A1: ( S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} ) ; :: thesis: o1 = o2
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o1 ) by A1, Def8;
then the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:25;
hence o1 = o2 by A1, Def4; :: thesis: verum