theorem :: ABCMIZ_1:138

for C being initialized ConstructorSignature
for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))