:: deftheorem defines at ABCMIZ_1:def 63 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence of QuasiTerms C holds p at f = (f #) * p;