theorem :: ABCMIZ_1:140

for C being initialized ConstructorSignature
for f being empty valuation of C holds f # = id (Union the Sorts of (Free (C,(MSVars C))))