theorem Th8: :: OSALG_1:8

for S being OrderSortedSign
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