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;
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