consider op being Element of on such that
A2: w <= the_arity_of op by A1;
set Lo = LBound (op,w);
LBound (op,w) has_least_args_for op,w by A2, Def14;
then op ~= LBound (op,w) ;
then A3: Name op = Name (LBound (op,w)) by Th31;
then A4: Name (LBound (op,w)) = on by Th33;
then reconsider Lo = LBound (op,w) as Element of on by Th33;
take Lo ; :: thesis: for op being Element of on st w <= the_arity_of op holds
Lo = LBound (op,w)
let op1 be Element of on; :: thesis: ( w <= the_arity_of op1 implies Lo = LBound (op1,w) )
assume A5: w <= the_arity_of op1 ; :: thesis: Lo = LBound (op1,w)
Name op1 = on by Th33;
then op1 ~= op by A3, A4, Th31;
hence Lo = LBound (op1,w) by A2, A5, Th34; :: thesis: verum