:: deftheorem Def62 defines at ABCMIZ_1:def 62 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds
p at f = (f #) * p;