let SR be monotone regular OrderSortedSign; :: thesis: 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; :: thesis: 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 * ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum