theorem Th114: :: ABCMIZ_1:114

for S being non void Signature
for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s )