theorem :: ABCMIZ_1:134

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
for f being valuation of C st len p = len (the_arity_of c) holds
(c -trm p) at f = c -trm (p at f) by Def60;