theorem Th131: :: ABCMIZ_1:131

for C being initialized ConstructorSignature
for X being Subset of Vars holds
( dom (C idval X) = X & ( for x being variable st x in X holds
(C idval X) . x = x -term C ) )