theorem Th127: :: ABCMIZ_1:127

for S being non void Signature
for X, Y being ManySortedSet of the carrier of S
for g1 being Symbol of (DTConMSA X)
for g2 being Symbol of (DTConMSA Y)
for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2