theorem Th149: :: ABCMIZ_1:149

for C being initialized ConstructorSignature
for e being expression of C
for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)