set m = [a_Type ,[{} ,0 ]];
set a = [an_Adj ,[{} ,0 ]];
( a_Type in {a_Type } & an_Adj in {an_Adj } & [(<*> Vars ),0 ] in [:QuasiLoci ,NAT :] ) by Th31, TARSKI:def 1, ZFMISC_1:def 2;
then ( [a_Type ,[{} ,0 ]] in Modes & [an_Adj ,[{} ,0 ]] in Attrs ) by ZFMISC_1:def 2;
then ( [a_Type ,[{} ,0 ]] in Modes \/ Attrs & [an_Adj ,[{} ,0 ]] in Modes \/ Attrs ) by XBOOLE_0:def 3;
then ( [a_Type ,[{} ,0 ]] in Constructors & [an_Adj ,[{} ,0 ]] in Constructors & the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors ) by MAXdef, XBOOLE_0:def 3;
then reconsider m = [a_Type ,[{} ,0 ]], a = [an_Adj ,[{} ,0 ]] as OperSymbol of MaxConstrSign by XBOOLE_0:def 3;
A1: ( m is constructor & a is constructor ) by CNSTR2;
take m ; :: according to ABCMIZ_1:def 12 :: thesis: ex a being OperSymbol of MaxConstrSign st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
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 = m `1 by A1, MAXdef
.= a_Type by MCART_1:7 ; :: thesis: ( the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
len (the_arity_of m) = card ((m `2 ) `1 ) by A1, MAXdef
.= card ([{} ,0 ] `1 ) by MCART_1:7
.= 0 by CARD_1:47, MCART_1:7 ;
hence the_arity_of m = {} ; :: thesis: ( the_result_sort_of a = an_Adj & the_arity_of a = {} )
thus the_result_sort_of a = a `1 by A1, MAXdef
.= an_Adj by MCART_1:7 ; :: thesis: the_arity_of a = {}
len (the_arity_of a) = card ((a `2 ) `1 ) by A1, MAXdef
.= card ([{} ,0 ] `1 ) by MCART_1:7
.= 0 by CARD_1:47, MCART_1:7 ;
hence the_arity_of a = {} ; :: thesis: verum