let S1, S2 be standardized ConstructorSignature; ( the carrier' of S1 = the carrier' of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) )
assume A1:
the carrier' of S1 = the carrier' of S2
; ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
A2:
( the carrier of S1 = 3 & the carrier of S2 = 3 )
by ABCMIZ_1:def 9, YELLOW11:1;
then A3:
the Arity of S1 = the Arity of S2
by A1, A2, FUNCT_2:63;
hence
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
by A1, A2, A3, FUNCT_2:63; verum