theorem Th89: :: ABCMIZ_1:89

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for e being expression of C
for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
vars e = union { (vars t) where t is quasi-term of C : t in rng p }