theorem Th139: :: ABCMIZ_1:139

for C being initialized ConstructorSignature
for e being expression of C
for f being empty valuation of C holds e at f = e