theorem :: ABCMIZ_1:79

for C being initialized ConstructorSignature
for A1, A2 being finite Subset of (QuasiAdjs C)
for q1, q2 being pure expression of C, a_Type C st A1 ast q1 = A2 ast q2 holds
( A1 = A2 & q1 = q2 ) by XTUPLE_0:1;