theorem Th34: :: OSALG_1:34

for SR being 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)