theorem :: ABCMIZ_1:135

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