theorem Th51: :: ABCMIZ_1:51

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )