theorem :: ABCMIZ_1:148

for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C
for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)