theorem :: ABCMIZ_1:98

for C being initialized ConstructorSignature
for t being expression of C, a_Type C
for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t)