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;
A6:
the carrier of C2 = {a_Type,an_Adj,a_Term}
by A3;
A7:
the Arity of C1 . * = <*an_Adj,a_Type*>
by A1;
A8:
the Arity of C2 . * = <*an_Adj,a_Type*>
by A3;
A9:
the Arity of C1 . non_op = <*an_Adj*>
by A1;
A10:
the Arity of C2 . non_op = <*an_Adj*>
by A3;
A11:
the ResultSort of C1 . * = a_Type
by A1;
A12:
the ResultSort of C2 . * = a_Type
by A3;
A13:
the ResultSort of C1 . non_op = an_Adj
by A1;
A14:
the ResultSort of C2 . non_op = an_Adj
by A3;
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:66;
A18:
the Arity of C2 = (*,non_op) --> (<*an_Adj,a_Type*>,<*an_Adj*>)
by A8, A10, A16, FUNCT_4:66;
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:66;
hence
C1 = C2
by A2, A4, A5, A6, A12, A14, A17, A18, A20, FUNCT_4:66; verum