set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } is infinite
by Def12;
then consider m1, m2 being object such that
A3:
( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m1 <> m2 )
by ZFMISC_1:def 10;
consider o1 being OperSymbol of C such that
A4:
( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 1 )
by A3;
consider o2 being OperSymbol of C such that
A5:
( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 1 )
by A3;
reconsider m1 = m1, m2 = m2 as OperSymbol of s by A4, A5, ABCMIZ_1:def 32;
A6:
( m1 is unary & m2 is unary )
by A4, A5;
then A7:
( m1 <> ast C & m2 <> ast C )
by Th37;
( m1 <> non_op or m2 <> non_op )
by A3;
then
( m1 is constructor or m2 is constructor )
by A7;
hence
ex b1 being OperSymbol of s st
( b1 is unary & b1 is constructor )
by A6; verum