let SR be monotone regular OrderSortedSign; :: thesis: for o, o3, o4 being OperSymbol of SR
for w1 being Element of the carrier of SR * st o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 holds
o3 = o4
let o, o3, o4 be OperSymbol of SR; :: thesis: for w1 being Element of the carrier of SR * st o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 holds
o3 = o4
let w1 be Element of the carrier of SR * ; :: thesis: ( o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 implies o3 = o4 )
assume that
A1: o3 has_least_args_for o,w1 and
A2: o4 has_least_args_for o,w1 ; :: thesis: o3 = o4
A3: o ~= o3 by A1;
A4: o ~= o4 by A2;
then A5: o3 ~= o4 by A3, Th2;
w1 <= the_arity_of o3 by A1;
then A6: the_arity_of o4 <= the_arity_of o3 by A2, A3;
then A7: the_result_sort_of o4 <= the_result_sort_of o3 by A5, Def7;
w1 <= the_arity_of o4 by A2;
then A8: the_arity_of o3 <= the_arity_of o4 by A1, A4;
then A9: the_arity_of o3 = the_arity_of o4 by A6, Th6;
the_result_sort_of o3 <= the_result_sort_of o4 by A5, A8, Def7;
then the_result_sort_of o3 = the_result_sort_of o4 by A7, ORDERS_2:2;
hence o3 = o4 by A5, A9, Def3; :: thesis: verum