:: deftheorem Def60 defines # ABCMIZ_1:def 60 :
for C being initialized ConstructorSignature
for f being valuation of C
for b₃ being term-transformation of C, MSVars C holds
( b₃ = f # iff ( ( for x being variable holds
( ( x in dom f implies b₃ . (x -term C) = f . x ) & ( not x in dom f implies b₃ . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b₃ * p holds
b₃ . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b₃ . ((non_op C) term a) = (non_op C) term (b₃ . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b₃ . ((ast C) term (a,t)) = (ast C) term ((b₃ . a),(b₃ . t)) ) ) );