let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S st S is discrete & o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 holds
o1 = o2
let o1, o2 be OperSymbol of S; :: thesis: ( S is discrete & o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 implies o1 = o2 )
assume A1: S is discrete ; :: thesis: ( not o1 ~= o2 or not the_arity_of o1 <= the_arity_of o2 or not the_result_sort_of o1 <= the_result_sort_of o2 or o1 = o2 )
then reconsider S1 = S as discrete OrderSortedSign ;
reconsider s1 = the_result_sort_of o1, s2 = the_result_sort_of o2 as SortSymbol of S1 ;
assume that
A2: o1 ~= o2 and
A3: the_arity_of o1 <= the_arity_of o2 and
A4: the_result_sort_of o1 <= the_result_sort_of o2 ; :: thesis: o1 = o2
A5: s1 = s2 by A4, ORDERS_3:1;
the_arity_of o1 = the_arity_of o2 by A1, A3, Th7;
hence o1 = o2 by A2, A5, Def3; :: thesis: verum