theorem :: ABCMIZ_1:147

for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C holds
( adjs (T at f) = (adjs T) at f & the_base_of (T at f) = (the_base_of T) at f ) ;