theorem :: ABCMIZ_1:136

for C being initialized ConstructorSignature
for t being expression of C, a_Type C
for a being expression of C, an_Adj C
for f being valuation of C holds ((ast C) term (a,t)) at f = (ast C) term ((a at f),(t at f)) by Def60;