let C be ConstructorSignature; :: thesis: ( C is arity-rich implies C is initialized )
assume A0: C is arity-rich ; :: thesis: C is initialized
set Xt = { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
consider x being Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } is infinite set by A0, ARdef;
then x in { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
then consider m being OperSymbol of C such that
A1: ( x = m & the_result_sort_of m = a_Type C & len (the_arity_of m) = 0 ) ;
set Xa = { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
consider x being Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } is infinite set by A0, ARdef;
then x in { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
then consider a being OperSymbol of C such that
A2: ( x = a & the_result_sort_of a = an_Adj C & len (the_arity_of a) = 0 ) ;
take m ; :: according to ABCMIZ_1:def 12 :: thesis: ex b₁ being Element of the carrier' of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b₁ = an_Adj & the_arity_of b₁ = {} )
take a ; :: thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
thus ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A1, A2; :: thesis: verum