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, Def15;
then A5: op1 ~= LBound op1,w by Def10;
A6: LBound op2,w has_least_args_for op2,w by A3, Def15;
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 by Def10;
op2 ~= LBound op2,w by A6, Def10;
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, Def10;
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, Def8;
w <= the_arity_of (LBound op2,w) by A6, Def10;
then A12: the_arity_of (LBound op1,w) <= the_arity_of (LBound op2,w) by A4, A8, Def10;
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, Def8;
then the_result_sort_of (LBound op1,w) = the_result_sort_of (LBound op2,w) by A11, ORDERS_2:25;
hence LBound op1,w = LBound op2,w by A9, A13, Def4; :: thesis: verum