let C1, C2 be strict Signature; ( 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
and
A2:
the carrier' of C1 = {* ,non_op }
and
A3:
C2 is constructor
and
A4:
the carrier' of C2 = {* ,non_op }
; C1 = C2
set A = {a_Type ,an_Adj ,a_Term };
A5:
the carrier of C1 = {a_Type ,an_Adj ,a_Term }
by A1, Def9;
A6:
the carrier of C2 = {a_Type ,an_Adj ,a_Term }
by A3, Def9;
A7:
the Arity of C1 . * = <*an_Adj ,a_Type *>
by A1, Def9;
A8:
the Arity of C2 . * = <*an_Adj ,a_Type *>
by A3, Def9;
A9:
the Arity of C1 . non_op = <*an_Adj *>
by A1, Def9;
A10:
the Arity of C2 . non_op = <*an_Adj *>
by A3, Def9;
A11:
the ResultSort of C1 . * = a_Type
by A1, Def9;
A12:
the ResultSort of C2 . * = a_Type
by A3, Def9;
A13:
the ResultSort of C1 . non_op = an_Adj
by A1, Def9;
A14:
the ResultSort of C2 . non_op = an_Adj
by A3, Def9;
A15:
dom the Arity of C1 = {* ,non_op }
by A2, FUNCT_2:def 1;
A16:
dom the Arity of C2 = {* ,non_op }
by A4, FUNCT_2:def 1;
A17:
the Arity of C1 = * ,non_op --> <*an_Adj ,a_Type *>,<*an_Adj *>
by A7, A9, A15, FUNCT_4:69;
A18:
the Arity of C2 = * ,non_op --> <*an_Adj ,a_Type *>,<*an_Adj *>
by A8, A10, A16, FUNCT_4:69;
A19:
dom the ResultSort of C1 = {* ,non_op }
by A1, A2, FUNCT_2:def 1;
A20:
dom the ResultSort of C2 = {* ,non_op }
by A3, A4, FUNCT_2:def 1;
the ResultSort of C1 = * ,non_op --> a_Type ,an_Adj
by A11, A13, A19, FUNCT_4:69;
hence
C1 = C2
by A2, A4, A5, A6, A12, A14, A17, A18, A20, FUNCT_4:69; verum