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 & len (the_arity_of op1) = len (the_arity_of 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 & len (the_arity_of op1) = len (the_arity_of 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 & len (the_arity_of op1) = len (the_arity_of op2) & w <= the_arity_of op1 & w <= the_arity_of op2 implies LBound op1,w = LBound op2,w )
assume A1: ( op1 ~= op2 & len (the_arity_of op1) = len (the_arity_of op2) & w <= the_arity_of op1 & w <= the_arity_of op2 ) ; :: thesis: LBound op1,w = LBound op2,w
set Lo1 = LBound op1,w;
set Lo2 = LBound op2,w;
A2: ( LBound op1,w has_least_args_for op1,w & LBound op2,w has_least_args_for op2,w ) by A1, Def15;
then A3: ( op1 ~= LBound op1,w & w <= the_arity_of (LBound op1,w) & ( for o2 being OperSymbol of SR st op1 ~= o2 & w <= the_arity_of o2 holds
the_arity_of (LBound op1,w) <= the_arity_of o2 ) ) by Def10;
A4: ( op2 ~= LBound op2,w & w <= the_arity_of (LBound op2,w) & ( 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 A2, Def10;
then A5: ( op1 ~= LBound op2,w & op2 ~= LBound op1,w ) by A1, A3, Th2;
then A6: LBound op1,w ~= LBound op2,w by A3, Th2;
A7: ( the_arity_of (LBound op1,w) <= the_arity_of (LBound op2,w) & the_arity_of (LBound op2,w) <= the_arity_of (LBound op1,w) ) by A3, A4, A5;
then A8: the_arity_of (LBound op1,w) = the_arity_of (LBound op2,w) by Th6;
( the_result_sort_of (LBound op1,w) <= the_result_sort_of (LBound op2,w) & the_result_sort_of (LBound op2,w) <= the_result_sort_of (LBound op1,w) ) by A6, A7, Def8;
then the_result_sort_of (LBound op1,w) = the_result_sort_of (LBound op2,w) by ORDERS_2:25;
hence LBound op1,w = LBound op2,w by A6, A8, Def4; :: thesis: verum