set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } is infinite by Def12;
then consider m1, m2 being object such that
A1: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m1 <> m2 ) by ZFMISC_1:def 10;
consider o1 being OperSymbol of C such that
A2: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 0 ) by A1;
reconsider m1 = m1 as OperSymbol of s by A2, ABCMIZ_1:def 32;
the_arity_of m1 = {} by A2;
then m1 is nullary ;
hence ex b₁ being OperSymbol of s st
( b₁ is nullary & b₁ is constructor ) ; :: thesis: verum