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 A1: ( 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) )
A2: the carrier' of S c= the carrier' of C by INSTALG1:10;
reconsider c = o as OperSymbol of C by A2;
A3: c is constructor by A1;
( 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:12;
then ( the_result_sort_of c = the_result_sort_of o & the_arity_of c = the_arity_of o ) by FUNCT_1:49;
hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) by A3, Def1; :: thesis: verum