theorem :: ABCMIZ_1:133

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