:: deftheorem Def1 defines standardized ABCMIZ_A:def 1 :
for C being ConstructorSignature holds
( C is standardized iff for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) );