let C1, C2 be strict Signature; :: thesis: ( C1 is constructor & the carrier' of C1 = {* ,non_op } & C2 is constructor & the carrier' of C2 = {* ,non_op } implies C1 = C2 )
assume that
A1: ( C1 is constructor & the carrier' of C1 = {* ,non_op } ) and
A2: ( C2 is constructor & the carrier' of C2 = {* ,non_op } ) ; :: thesis: C1 = C2
set A = {a_Type ,an_Adj ,a_Term };
A3: ( the carrier of C1 = {a_Type ,an_Adj ,a_Term } & the carrier of C2 = {a_Type ,an_Adj ,a_Term } ) by A1, A2, CONSTRSIGN;
A4: ( the Arity of C1 . * = <*an_Adj ,a_Type *> & the Arity of C2 . * = <*an_Adj ,a_Type *> ) by A1, A2, CONSTRSIGN;
A5: ( the Arity of C1 . non_op = <*an_Adj *> & the Arity of C2 . non_op = <*an_Adj *> ) by A1, A2, CONSTRSIGN;
A6: ( the ResultSort of C1 . * = a_Type & the ResultSort of C2 . * = a_Type ) by A1, A2, CONSTRSIGN;
A7: ( the ResultSort of C1 . non_op = an_Adj & the ResultSort of C2 . non_op = an_Adj ) by A1, A2, CONSTRSIGN;
( dom the Arity of C1 = {* ,non_op } & dom the Arity of C2 = {* ,non_op } ) by A1, A2, FUNCT_2:def 1;
then A8: ( the Arity of C1 = * ,non_op --> <*an_Adj ,a_Type *>,<*an_Adj *> & the Arity of C2 = * ,non_op --> <*an_Adj ,a_Type *>,<*an_Adj *> ) by A4, A5, FUNCT_4:69;
( dom the ResultSort of C1 = {* ,non_op } & dom the ResultSort of C2 = {* ,non_op } ) by A1, A2, FUNCT_2:def 1;
then ( the ResultSort of C1 = * ,non_op --> a_Type ,an_Adj & the ResultSort of C2 = * ,non_op --> a_Type ,an_Adj ) by A6, A7, FUNCT_4:69;
hence C1 = C2 by A1, A2, A3, A8; :: thesis: verum