set m = [a_Type ,[{} ,0 ]];
set a = [an_Adj ,[{} ,0 ]];
A2: a_Type in {a_Type } by TARSKI:def 1;
A3: an_Adj in {an_Adj } by TARSKI:def 1;
A4: [(<*> Vars ),0 ] in [:QuasiLoci ,NAT :] by Th29, ZFMISC_1:def 2;
then A5: [a_Type ,[{} ,0 ]] in Modes by A2, ZFMISC_1:def 2;
A6: [an_Adj ,[{} ,0 ]] in Attrs by A3, A4, ZFMISC_1:def 2;
A7: [a_Type ,[{} ,0 ]] in Modes \/ Attrs by A5, XBOOLE_0:def 3;
A8: [an_Adj ,[{} ,0 ]] in Modes \/ Attrs by A6, XBOOLE_0:def 3;
A9: [a_Type ,[{} ,0 ]] in Constructors by A7, XBOOLE_0:def 3;
A10: [an_Adj ,[{} ,0 ]] in Constructors by A8, XBOOLE_0:def 3;
the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors by Def24;
then reconsider m = [a_Type ,[{} ,0 ]], a = [an_Adj ,[{} ,0 ]] as OperSymbol of MaxConstrSign by A9, A10, XBOOLE_0:def 3;
A11: m is constructor by Def11;
A12: a is constructor by Def11;
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 A11, Def24
.= 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 A11, Def24
.= 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 A12, Def24
.= an_Adj by MCART_1:7 ; :: thesis: the_arity_of a = {}
len (the_arity_of a) = card ((a `2 ) `1 ) by A12, Def24
.= card ([{} ,0 ] `1 ) by MCART_1:7
.= 0 by CARD_1:47, MCART_1:7 ;
hence the_arity_of a = {} ; :: thesis: verum