let o be OperSymbol of MaxConstrSign ; :: according to ABCMIZ_A:def 1 :: thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) ) )
A1: the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors by ABCMIZ_1:def 24;
assume A2: o is constructor ; :: thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) )
then A3: ( the ResultSort of MaxConstrSign . o = o `1 & card (the Arity of MaxConstrSign . o) = card ((o `2 ) `1 ) ) by ABCMIZ_1:def 24;
( o <> * & o <> non_op ) by A2, ABCMIZ_1:def 11;
then not o in {* ,non_op } by TARSKI:def 2;
hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) ) by A3, A1, XBOOLE_0:def 3; :: thesis: verum