theorem Th137: :: ABCMIZ_1:137

for C being initialized ConstructorSignature
for e being expression of C
for X being Subset of Vars holds e at (C idval X) = e