theorem :: ABCMIZ_1:141

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C
for f being valuation of C holds (Non a) at f = Non (a at f)