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
; for op being Element of on st w <= the_arity_of op holds
Lo = LBound (op,w)
let op1 be Element of on; ( w <= the_arity_of op1 implies Lo = LBound (op1,w) )
assume A5:
w <= the_arity_of op1
; 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; verum