theorem :: ABCMIZ_1:151

for C being initialized ConstructorSignature
for T being quasi-type of C
for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)