theorem :: ABCMIZ_1:90

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }