:: deftheorem defines at ABCMIZ_1:def 61 :
for C being initialized ConstructorSignature
for f being valuation of C
for e being expression of C holds e at f = (f #) . e;