let C be ConstructorSignature; :: thesis: ( C is arity-rich implies C is initialized )
assume A3: 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 ) } ;
set x = the 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 A3;
then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } 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
A4: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } = 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 ) } ;
set x = the 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 A3;
then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } 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
A5: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } = 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 A4, A5; :: thesis: verum