theorem Th52: :: ABCMIZ_1:52

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
c -trm p is expression of C, the_result_sort_of c