theorem Th88: :: ABCMIZ_1:88

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
variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }