let S be constructor Subsignature of C; :: thesis: S is standardized
let o be OperSymbol of S; :: 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) ) )
assume A0: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def 11 :: thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) )
A1: the carrier' of S c= the carrier' of C by INSTALG1:11;
o in the carrier' of S ;
then reconsider c = o as OperSymbol of C by A1;
A2: c is constructor by A0, ABCMIZ_1:def 11;
( the Arity of S = the Arity of C | the carrier' of S & the ResultSort of S = the ResultSort of C | the carrier' of S ) by INSTALG1:13;
then ( the_result_sort_of c = the_result_sort_of o & the_arity_of c = the_arity_of o ) by FUNCT_1:72;
hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2 ) `1 ) = len (the_arity_of o) ) by A2, StandardizedDef; :: thesis: verum