let op1, op2 be Element of on; :: thesis: ( ( for op being Element of on st w <= the_arity_of op holds
op1 = LBound (op,w) ) & ( for op being Element of on st w <= the_arity_of op holds
op2 = LBound (op,w) ) implies op1 = op2 )
assume that
A6: for op3 being Element of on st w <= the_arity_of op3 holds
op1 = LBound (op3,w) and
A7: for op3 being Element of on st w <= the_arity_of op3 holds
op2 = LBound (op3,w) ; :: thesis: op1 = op2
consider op being Element of on such that
A8: w <= the_arity_of op by A1;
op1 = LBound (op,w) by A8, A6;
hence op1 = op2 by A8, A7; :: thesis: verum