theorem Th59: :: ABCMIZ_A:59

for X being finite Subset of Vars st varcl X = X holds
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )