theorem Th55: :: ABCMIZ_1:55

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for a being expression of C, an_Adj C
for t being expression of C, a_Type C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)