theorem Th75: :: ABCMIZ_1:75

for C being initialized ConstructorSignature
for p being FinSequence of QuasiTerms C
for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds
m -trm p is pure expression of C, a_Type C