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, Def15;
then op ~= LBound op,w by Def10;
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