set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } ;
not { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } is finite
by ARdef;
then consider m1, m2 being set such that
A1:
( 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 REALSET1:14;
consider o1 being OperSymbol of C such that
A2:
( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 1 )
by A1;
consider o2 being OperSymbol of C such that
A3:
( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 1 )
by A1;
reconsider m1 = m1, m2 = m2 as OperSymbol of s by A2, A3, ABCMIZ_1:def 32;
A5:
( m1 is unary & m2 is unary )
by A2, A3, Udef;
then A4:
( m1 <> ast C & m2 <> ast C )
by ThDiff;
( m1 <> non_op or m2 <> non_op )
by A1;
then
( m1 is constructor or m2 is constructor )
by A4, ABCMIZ_1:def 11;
hence
ex b1 being OperSymbol of s st
( b1 is unary & b1 is constructor )
by A5; verum