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 ;
A12: a is constructor ;
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 ; :: 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)
.= 0 ;
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 ; :: thesis: the_arity_of a = {}
len (the_arity_of a) = card ((a `2) `1) by A12, Def24
.= card ([{},0] `1)
.= 0 ;
hence the_arity_of a = {} ; :: thesis: verum