let C be ConstructorSignature; :: thesis: ( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) )
hereby :: thesis: ( ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) implies C is initialized )
assume C is initialized ; :: thesis: ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
then consider m, a being OperSymbol of C such that
A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) ;
reconsider m = m as OperSymbol of a_Type C by A1, ABCMIZ_1:def 32;
reconsider a = a as OperSymbol of an_Adj C by A1, ABCMIZ_1:def 32;
take m = m; :: thesis: ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
take a = a; :: thesis: ( m is nullary & a is nullary )
thus m is nullary by A1; :: thesis: a is nullary
thus a is nullary by A1; :: thesis: verum
end;
given m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A2: ( m is nullary & a is nullary ) ; :: thesis: C is initialized
take m ; :: according to ABCMIZ_1:def 12 :: thesis: ex b1 being Element of the carrier' of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b1 = an_Adj & the_arity_of b1 = {} )
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 = {} )
( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38;
hence ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A2, ABCMIZ_1:def 32; :: thesis: verum