theorem :: ABCMIZ_1:132

for C being initialized ConstructorSignature
for f being valuation of C
for x being variable st not x in dom f holds
(x -term C) at f = x -term C by Def60;