let SR be monotone regular OrderSortedSign; for op1, op2 being OperSymbol of SR
for w being Element of the carrier of SR * st op1 ~= op2 & w <= the_arity_of op1 & w <= the_arity_of op2 holds
LBound (op1,w) = LBound (op2,w)
let op1, op2 be OperSymbol of SR; for w being Element of the carrier of SR * st op1 ~= op2 & w <= the_arity_of op1 & w <= the_arity_of op2 holds
LBound (op1,w) = LBound (op2,w)
let w be Element of the carrier of SR * ; ( op1 ~= op2 & w <= the_arity_of op1 & w <= the_arity_of op2 implies LBound (op1,w) = LBound (op2,w) )
assume that
A1:
op1 ~= op2
and
A2:
w <= the_arity_of op1
and
A3:
w <= the_arity_of op2
; LBound (op1,w) = LBound (op2,w)
set Lo1 = LBound (op1,w);
set Lo2 = LBound (op2,w);
A4:
LBound (op1,w) has_least_args_for op1,w
by A2, Def14;
then A5:
op1 ~= LBound (op1,w)
;
A6:
LBound (op2,w) has_least_args_for op2,w
by A3, Def14;
then A7:
for o2 being OperSymbol of SR st op2 ~= o2 & w <= the_arity_of o2 holds
the_arity_of (LBound (op2,w)) <= the_arity_of o2
;
op2 ~= LBound (op2,w)
by A6;
then A8:
op1 ~= LBound (op2,w)
by A1, Th2;
then A9:
LBound (op1,w) ~= LBound (op2,w)
by A5, Th2;
w <= the_arity_of (LBound (op1,w))
by A4;
then A10:
the_arity_of (LBound (op2,w)) <= the_arity_of (LBound (op1,w))
by A1, A5, A7, Th2;
then A11:
the_result_sort_of (LBound (op2,w)) <= the_result_sort_of (LBound (op1,w))
by A9, Def7;
w <= the_arity_of (LBound (op2,w))
by A6;
then A12:
the_arity_of (LBound (op1,w)) <= the_arity_of (LBound (op2,w))
by A4, A8;
then A13:
the_arity_of (LBound (op1,w)) = the_arity_of (LBound (op2,w))
by A10, Th6;
the_result_sort_of (LBound (op1,w)) <= the_result_sort_of (LBound (op2,w))
by A9, A12, Def7;
then
the_result_sort_of (LBound (op1,w)) = the_result_sort_of (LBound (op2,w))
by A11, ORDERS_2:2;
hence
LBound (op1,w) = LBound (op2,w)
by A9, A13, Def3; verum